作为HOL片段的规范性条件推理

我们报告了（基于偏好的）条件规范性推理的机械化。我们的重点在于Aqvist的条件义务系统E及其扩展。我们的机械化是通过在Isabelle/HOL中的浅层语义嵌入实现的。我们考虑了该框架的两种可能用途。第一种是作为对所考虑逻辑进行元推理的工具。我们将其用于自动验证道义对应关系（广义上理解）及相关问题，类似于先前针对模态逻辑立方体所完成的工作。等价性在一个方向上被自动验证，即从性质导向公理。第二种用途是作为评估伦理论证的工具。我们提供了人口伦理学中一个著名悖论（或不可能定理）——Parfit的令人厌恶的结论——的计算机编码。虽然有人提出通过放弃预设的“优于”的传递性来克服该不可能定理，但我们的形式化揭示了一种不那么极端的方法，除其他外，建议适当地弱化传递性而非完全抛弃它。所呈现的编码是否增加或减少令人厌恶结论的吸引力与说服力，是我们希望交由哲学与伦理学来回答的问题。