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

In M. Baldoni, M. Dastani, B. Liao, Y. Sakurai & R. Zalila Wenkstern (eds.), PRIMA 2019: Principles and Practice of Multi-Agent Systems. 93413 Cham, Germany: Springer. pp. 202-218 (2019)
Download Edit this record How to cite View on PhilPapers
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.
Categories
(categorize this paper)
PhilPapers/Archive ID
LYOAAR
Upload history
Archival date: 2020-02-03
View other versions
Added to PP index
2019-10-31

Total views
71 ( #40,175 of 52,923 )

Recent downloads (6 months)
53 ( #11,241 of 52,923 )

How can I increase my downloads?

Downloads since first upload
This graph includes both downloads from PhilArchive and clicks on external links on PhilPapers.