Proof Theory and Decision Procedures for Deontic STIT Logics

TL;DR

This paper provides a set of cut-free complete sequent-style calculi for deontic STIT logics used to formally reason about choice-making, obligations, and norms in a multi-agent setting and develops a syntactic decision procedure for this class of logics.

Abstract

This paper provides a set of cut-free complete sequent-style calculi for deontic STIT ('See To It That') logics used to formally reason about choice-making, obligations, and norms in a multi-agent setting. We leverage these calculi to write a proof-search algorithm deciding deontic, multi-agent STIT logics with (un)limited choice and introduce a loop-checking mechanism to ensure the termination of the algorithm. Despite the acknowledged potential for deontic reasoning in the context of autonomous, multi-agent scenarios, this work is the first to provide a syntactic decision procedure for this class of logics. Our proof-search procedure is designed to provide verifiable witnesses/certificates of the (in)validity of formulae, which permits an analysis of the (non)theoremhood of formulae and act as explanations thereof. We show how the proof system and decision algorithm can be used to automate normative reasoning tasks such as duty checking (viz. determining an agent's obligations relative to a given knowledge base), compliance checking (viz. determining if a choice, considered by an agent as potential conduct, complies with the given knowledge base), and joint fulfillment checking (viz. determining whether under a specified factual context an agent can jointly fulfill all their duties).

Figures (6)

• Figure 1: An illustration of the $\mathsf{DS}_{n}$-model $M := (F,V)$ built atop the $\mathsf{DS}_{n}$-frame $F := (W,\{R_{[j]}, R_{[y]}\},\{I_{\otimes_{j}}, I_{\otimes_{y}}\})$ such that $W := \{w_{1}, w_{2}, w_{3}, w_{4}\}$, $R' := \{(w_{i},w_{i}) \ | \ 1 \leq i \leq 4\}$, Jade's relation $R_{[j]} := \{(w_{1}, w_{3}), (w_{3}, w_{1}), (w_{2}, w_{4}), (w_{4}, w_{2})\} \cup R'$, Kai's relation $R_{[k]} := \{(w_{1}, w_{2}), (w_{2}, w_{1}), (w_{3}, w_{4}), (w_{4}, w_{3})\} \cup R'$, $I_{\otimes_{j}} := \{w_{1},w_{3}\}$, $I_{\otimes_{k}} := \{w_{1},w_{2}\}$, and $V := \{(\texttt{left}\_\texttt{jade},\{w_{1},w_{3}\}),(\texttt{right}\_\texttt{jade},\{w_{2},w_{4}\}),(\texttt{left}\_\texttt{kai},\{w_{1},w_{2}\}),(\texttt{right}\_\texttt{kai},\{w_{3},w_{4}\}),(\texttt{coll},\{w_{2},w_3\})\}$.
• Figure 2: The $\mathsf{G3DS}_{n}^{k}$ calculi Lyo21thesis, where $|Ag| = n \in \mathbb{N}$ and $k \in \mathbb{N}$. The superscript $\dag$ on $(\Box)$, $([i])$, $(\otimes_{i})$, $(\mathsf{IOA})$, and $(\mathsf{D2}_{i})$ indicates that $u$ is a eigenvariable, i.e. it does not occur in the conclusion. We have $(\langle i \rangle)$, $([i])$, $(\ominus_{i})$, $(\otimes_{i})$, $(\mathsf{Ref}_{i})$, $(\mathsf{Euc}_{i})$, $(\mathsf{APC}_{i}^{k})$, $(\mathsf{D2}_{i})$, and $(\mathsf{D3}_{i})$ rules for each $i \in Ag$. $(\mathsf{APC}_{i}^{k})$ is omitted when $k = 0$.
• Figure 3: The set $\mathsf{StrR}$ of structural rules consists of the rules above.
• Figure 4: Admissible rules. The side condition $\dag$ stipulates that $v$ must be an eigenvariable.
• Figure 5: Three 'snapshots' of proof-search without loop-checking, showing that proof-search will continue ad infinitum if loop-checking is not enforced.

Theorems & Definitions (36)

• Definition 1: The Language $\mathcal{L}_{n}$
• Definition 2: $\mathsf{DS}_{n}^{k}$-frames, -models
• Definition 3: Semantics
• Definition 4: Sequent
• Example 5
• Definition 6: Sequent Semantics
• Theorem 7: $\mathsf{G3DS}_{n}^{k}$ Properties Lyo21thesis
• Definition 8: $\mathcal{R}^{i}$-Path
• Lemma 9
• Definition 10: Thread