Automating Agential Reasoning: Proof-Calculi and Syntactic Decidability for STIT Logics

This work provides proof-search algorithms and automated counter-model extraction for a class of STIT logics. With this, we answer an open problem concerning syntactic decision procedures and cut-free calculi for STIT logics. A new class of cut-free complete labelled sequent calculi G3LdmL^m_n, for multi-agent STIT with at most n-many choices, is introduced. We refine the calculi G3LdmL^m_n through the use of propagation rules and demonstrate the admissibility of their structural rules, resulting in auxiliary calculi Ldm^m_nL. In the single-agent case, we show that the refined calculi Ldm^m_nL derive theorems within a restricted class of (forestlike) sequents, allowing us to provide proof-search algorithms that decide single-agent STIT logics. We prove that the proof-search algorithms are correct and terminate.

Cut-free Calculi and Relational Semantics for Temporal STIT Logics

We present cut-free labelled sequent calculi for a central formalism in logics of agency: STIT logics with temporal operators. These include sequent systems for Ldm, Tstit and Xstit. All calculi presented possess essential structural properties such as contraction- and cut-admissibility. The labelled calculi G3Ldm and G3TSTIT are shown sound and complete relative to irreflexive temporal frames. Additionally, we extend current results by showing that also XSTIT can be characterized through relational frames, omitting the use of BT+AC frames.

Appendix for: Cut-free Calculi and Relational Semantics for Temporal STIT logics

This paper is an appendix to the paper "Cut-free Calculi and Relational Semantics for Temporal STIT logics" by Berkel and Lyon, 2019. It provides the completeness proof for the basic STIT logic Ldm (relative to irreflexive, temporal Kripke STIT frames) as well as gives the derivation of the independence of agents axiom for the logic Xstit.