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

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 29 Aug 2019.

## Built on by (most cited first, 2 of 2)

- [Automating Reasoning with Standpoint Logic via Nested Sequents](https://mlsanity.com/paper/2205.02749/) (2022)
- [Uniform and Modular Sequent Systems for Description Logics](https://mlsanity.com/paper/2206.09020/) (2022)

## Abstract (arXiv)

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.