Automating Agential Reasoning: Proof-Calculi and Syntactic Decidability for STIT Logics
Abstract
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.
Cite
@article{arxiv.1908.11360,
title = {Automating Agential Reasoning: Proof-Calculi and Syntactic Decidability for STIT Logics},
author = {Tim Lyon and Kees van Berkel},
journal= {arXiv preprint arXiv:1908.11360},
year = {2020}
}
Comments
Included version of the paper "Automating Agential Reasoning: Proof-Calculi and Syntactic Decidability for STIT Logics", accepted to the 22nd International Conference on Principles and Practice of Multi-Agent Systems (PRIMA 2019)