A Reduction of Input/Output Logics to SAT

It studies reasoning patterns and logical properties that are not suitably captured by classical propositional or first-order logic. Various logic formalisms have been proposed to handle deontic and normative reasoning, including systems based on modal logics (von Wright, 1951), dyadic deontic logic (Gabbay et al., 2013), and norm-based systems (Hansen, 2014). These systems differ in the properties of the obligation operator, and in their ability to consistently handle deontic paradoxes and/or norm conflicts (Gabbay et al., 2013). Input/Output (I/O) logics (Makinson & van der Torre, 2000) are a particular norm-based family of systems in which conditional norms are represented by pairs of formulas. The pairs do not carry truth-values themselves. I/O logics use an operational semantics based on detachment and come with a variety of different systems, formalized by different so-called output operators . Given a set of conditional norms N, and a set of formulas describing the situational context A, output operators produce a set of formulas that represent the obligations that are in force for that context. In order to check whether some state of affairs φ is obligatory, it suffices to check whether φ out (N, A), where out is some output operator. Unconstrained I/O logics are monotone and cannot consistently handle norm conflicts (i.e., situations in which norms with conflicting obligations are in force) without