将输入输出逻辑转化为可满足性问题，实现自动化推理
A Reduction of Input/Output Logics to SAT
- 将条件规范转化为命题逻辑可满足性问题求解
- 提出原型系统rio，支持规范推理的自动执行
- 适合形式化规范分析与合规性验证的研究者
道义逻辑是用于规范、义务、许可和禁止推理的形式系统。输入/输出（I/O）逻辑是一类基于规范的道义逻辑，其在基础对象逻辑语言之外形式化条件规范，且条件规范本身不具有真值。本文提出一种自动化方法，通过将I/O逻辑问题转化为（一系列）命题可满足性问题来求解。文章介绍了该方法的原型实现rio（输入/输出逻辑求解器），并应用于多个示例进行说明。
原文摘要 · Abstract (English)
Deontic logics are formalisms for reasoning over norms, obligations, permissions and prohibitions. Input/Output (I/O) Logics are a particular family of so-called norm-based deontic logics that formalize conditional norms outside of the underlying object logic language, where conditional norms do not carry a truth-value themselves. In this paper, an automation approach for I/O logics is presented that makes use of suitable reductions to (sequences of) propositional satisfiability problems. A prototypical implementation, named rio (reasoner for input/output logics), of the proposed procedures is presented and applied to illustrative examples.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。