A Reduction of Input/Output Logics to SAT
This work addresses the problem of automating deontic logic reasoning for researchers and practitioners in formal logic and AI, but it appears incremental as it applies existing SAT techniques to a specific logic family.
The paper tackled the automation of reasoning in Input/Output (I/O) logics, which are used for formalizing conditional norms, by developing a reduction to propositional satisfiability (SAT) problems, resulting in a prototypical implementation called rio that was applied to illustrative examples.
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.