Automating Agential Reasoning: Proof-Calculi and Syntactic Decidability for STIT Logics
Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/Gutachten › Beitrag in Konferenzband › Beigetragen › Begutachtung
Beitragende
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.
Details
Originalsprache | Englisch |
---|---|
Titel | PRIMA 2019: Principles and Practice of Multi-Agent Systems |
Redakteure/-innen | Matteo Baldoni, Mehdi Dastani, Beishui Liao, Yuko Sakurai, Rym Zalila Wenkstern |
Erscheinungsort | Cham |
Herausgeber (Verlag) | Springer International Publishing AG |
Seiten | 202-218 |
Seitenumfang | 17 |
ISBN (Print) | 978-3-030-33792-6 |
Publikationsstatus | Veröffentlicht - 2019 |
Peer-Review-Status | Ja |
Externe IDs
Scopus | 85076502113 |
---|---|
ORCID | /0000-0003-3214-0828/work/142249483 |