# A Reduction of Input/Output Logics to SAT

arXiv: https://arxiv.org/abs/2508.16242 · HTML: https://mlsanity.com/paper/2508.16242/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 5 of its 49 references that are in the map.
- First posted on arXiv 22 Aug 2025.

## Builds on (most cited first, 5 of 5)

- [Recursive Online Enumeration of All Minimal Unsatisfiable Subsets](https://mlsanity.com/paper/1708.00400/) (2017)
- [Automated Reasoning in Non-classical Logics in the TPTP World](https://mlsanity.com/paper/2202.09836/) (2022)
- [Bridging between LegalRuleML and TPTP for Automated Normative Reasoning (extended version)](https://mlsanity.com/paper/2209.05090/) (2022)
- [Streamlining Input/Output Logics with Sequent Calculi](https://mlsanity.com/paper/2306.09496/) (2023)
- [TPTP World Infrastructure for Non-classical Logics](https://mlsanity.com/paper/2508.09318/) (2025)

## Abstract (arXiv)

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.