We report on the mechanization of (preference-based) conditional normative 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 equivalence is automatically verified in one direction, leading from the property to the axiom. The second use is as a tool for assessing ethical arguments. We provide a computer encoding of a well-known paradox (or impossibility theorem) in population ethics, Parfit's repugnant conclusion. While some have proposed overcoming the impossibility theorem by abandoning the presupposed transitivity of ''better than'', our formalisation unveils a less extreme approach, suggesting among other things the option of weakening transitivity suitably rather than discarding it entirely. 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.

翻译：本文报告了（基于偏好的）条件规范性推理的机械化实现。我们重点关注Åqvist的条件义务系统E及其扩展。我们的机械化是通过在Isabelle/HOL中的浅层语义嵌入实现的。我们探讨了该框架的两种可能用途：首先是作为所考虑逻辑的元推理工具，我们将其用于道义对应关系（广义理解）及相关问题的自动化验证，类似于先前在模态逻辑立方体研究中已实现的成果。等价性在一个方向上被自动验证，即从属性到公理的推导。其次是作为伦理论证评估工具，我们对人口伦理学中一个著名的悖论（或不可能性定理）——帕菲特的"令人厌恶的结论"进行了计算机编码。虽然有人提议通过放弃"优于"关系的传递性预设来克服该不可能性定理，但我们的形式化揭示了一种不那么极端的方法，特别提出了适当弱化而非完全抛弃传递性的可能方案。所呈现的编码究竟是增强还是削弱了"令人厌恶的结论"的吸引力和说服力，这个问题我们愿意留给哲学和伦理学领域来探讨。