A Reduction of Input/Output Logics to SAT

TL;DR

An automation approach for I/O logics is presented that makes use of suitable reductions to (sequences of) propositional satisfiability problems, and a prototypical implementation, named rio (reasoner for input/output logics), of the proposed procedures is presented.

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.

Figures (7)

• Figure 1: Construction of base $\mathbf{B}_3(N, A)$ using fixed-point iteration.
• Figure 2: Procedure for generating $\mathit{maxfamily}_\mathit{out}(N,A,C)$ where $\mathbf{B}(N,A)$ is the finite basis for the output operator $\mathit{out}$.
• Figure 3: Procedure for generating $\mathit{gout}(N,A,C,\mathit{out},\mathcal{S},\mathcal{A})$. In the first line, the procedure for generating the maxfamily from Fig.\ref{['fig:constrained']} is reused.
• Figure 4: Problem representation in unconstrained I/O logic without conjectures. The finite basis of $\mathit{out}_4(N,A)$, with $A = \{\textit{parking}\}$ and $N = \{ (\textit{parking}, \textit{ticket} \lor \textit{fine}), (\textit{ticket}, \textit{pay}), (\textit{fine}, \textit{pay}) \}$, is calculated. The output is depicted in Fig. \ref{['fig:result']}.
• Figure 5: Problem representation in constrained I/O logic with two conjectures. The problem is to decide whether $\neg\textit{telling} \in \mathit{out}^C_\cap(N,A)$ and $\neg\textit{helping} \in \mathit{out}^C_\cap(N,A)$, where $\mathit{out} = \mathit{out}_3$, $A = \{ \neg\textit{helping} \}$ and $N = \{ (\top, \textit{helping}), (\textit{helping}, \textit{telling}), (\neg\textit{helping}, \neg\textit{telling}) \}$. The output is depicted in Fig. \ref{['fig:result2']}.

Theorems & Definitions (15)

• Example 2.1
• Example 2.2: Contrary-to-duty
• Example 2.3: Contrary-to-duty, continued
• Definition 3.1: Directly Triggered Norm
• Theorem 3.2
• Theorem 3.3
• Definition 3.4: Weakly Triggered Set of Norms
• Theorem 3.5
• Theorem 3.6
• Lemma 3.7