Automating Agential Reasoning: Proof-Calculi and Syntactic Decidability for STIT Logics
This work addresses the automation of agential reasoning in formal logic, which is incremental as it builds on existing STIT frameworks.
The authors tackled the problem of automating reasoning in STIT logics by developing proof-search algorithms and automated counter-model extraction, answering an open problem about syntactic decision procedures and cut-free calculi. They introduced new cut-free labelled sequent calculi and refined them with propagation rules, proving correctness and termination for single-agent cases.
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.