We report some results regarding the mechanization of normative (preference-based) conditional reasoning. Our focus is on Aqvist's system E for conditional obligation (and its extensions). Our mechanization is achieved via a shallow semantical embedding in Isabelle/HOL. We consider two possible uses of the framework. The first one is as a tool for meta-reasoning about the considered logic. We employ it for the automated verification of deontic correspondences (broadly conceived) and related matters, analogous to what has been previously achieved for the modal logic cube. The second use is as a tool for assessing ethical arguments. We provide a computer encoding of a well-known paradox in population ethics, Parfit's repugnant conclusion. Whether the presented encoding increases or decreases the attractiveness and persuasiveness of the repugnant conclusion is a question we would like to pass on to philosophy and ethics.

翻译：我们报告了关于规范（基于偏好）条件推理机械化的一些结果。我们的重点在于Aqvist的规范义务系统E（及其扩展）。我们通过将浅语义嵌入到Isabelle/HOL中实现了机械化。我们考虑了该框架的两种可能用途。第一种是作为对所考虑逻辑进行元推理的工具。我们将其用于道义对应（广义上）及相关事项的自动验证，类似于之前在模态逻辑立方体中实现的结果。第二种用途是作为评估伦理论证的工具。我们提供了人口伦理学中一个著名悖论——帕菲特的令人反感的结论——的计算机编码。这一编码是否会增加或减少令人反感的结论的吸引力和说服力，是我们希望留给哲学和伦理学领域去探讨的问题。