A Reduction of Input/Output Logics to SAT

TL;DR

This paper introduces a method to automate Input/Output (I/O) deontic logics by reducing them to propositional satisfiability problems, enabling practical reasoning over norms.

Contribution

It presents a novel reduction approach for I/O logics to SAT problems and provides a prototype implementation called rio.

Findings

Successful reduction of I/O logics to SAT problems

Prototype tool rio demonstrates practical applicability

Illustrative examples validate the approach

Abstract

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.