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.

翻译：我们报告了基于偏好的条件规范推理的机械化实现。我们的重点在于Aqvist的条件义务系统E及其扩展。该机械化通过伊莎贝尔/HOL中的浅层语义嵌入实现。我们考虑了该框架的两种可能用途。第一种是作为所研究逻辑的元推理工具。我们将其用于义务对应关系（广义概念）及相关问题的自动验证，类似于先前在模态逻辑立方体中取得的成果。等价性在单一方向上自动验证，即从性质到公理的推导。第二种用途是作为评估伦理论证的工具。我们提供了人口伦理学中一个著名悖论（或不可能性定理）——帕菲特的“令人反感的结论”——的计算机编码。尽管有人提出通过放弃预设的"优于"关系的传递性来克服该不可能性定理，我们的形式化揭示了一种更为温和的解决方案，表明除其他可能性外，可以选择适当地弱化传递性而非完全抛弃它。该编码究竟是增加还是降低了"令人反感的结论"的吸引力和说服力，这是一个我们希望交由哲学与伦理学领域评判的问题。