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.

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