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)

Tim Lyon
Vienna University of Technology
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.
Keywords STIT  Multi-agent reasoning  Proof theory  Labelled calculi  Proof search  Decidability  Automated reasoning  Propagation rules  Logics of agency  Sequent
Categories (categorize this paper)
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

Proof Analysis in Modal Logic.Sara Negri - 2005 - Journal of Philosophical Logic 34 (5-6):507-544.
Complexity Results of STIT Fragments.François Schwarzentruber - 2012 - Studia Logica 100 (5):1001-1045.
Properties of Logics of Individual and Group Agency.Andreas Herzig & François Schwarzentruber - 2008 - In Carlos Areces & Robert Goldblatt (eds.), Advances in Modal Logic, Volume 7. CSLI Publications. pp. 133-149.

View all 8 references / Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles

Cut-Free Calculi and Relational Semantics for Temporal STIT Logics.Tim Lyon & Kees van Berkel - 2019 - In Francesco Calimeri, Nicola Leone & Marco Manna (eds.), Logics in Artificial Intelligence. Springer International Publishing. pp. 803 - 819.
Proof Theory for Quantified Monotone Modal Logics.Sara Negri & Eugenio Orlandelli - 2019 - Logic Journal of the IGPL 27 (4):478-506.
Labeled Sequent Calculi for Modal Logics and Implicit Contractions.Pierluigi Minari - 2013 - Archive for Mathematical Logic 52 (7-8):881-907.
Proofs and Countermodels in Non-Classical Logics.Sara Negri - 2014 - Logica Universalis 8 (1):25-60.
Bunched Logics Displayed.James Brotherston - 2012 - Studia Logica 100 (6):1223-1254.
A Neutral Temporal Deontic STIT Logic.Kees van Berkel & Tim Lyon - 2019 - In P. Blackburn, E. Lorini & M. Guo (eds.), Logic, Rationality, and Interaction. Berlin, Heidelberg: pp. 340-354.
Maehara-Style Modal Nested Calculi.Roman Kuznets & Lutz Straßburger - 2019 - Archive for Mathematical Logic 58 (3-4):359-385.
Proof Analysis in Modal Logic.Sara Negri - 2005 - Journal of Philosophical Logic 34 (5-6):507-544.
Sequent Calculi for Some Trilattice Logics.Norihiro Kamide & Heinrich Wansing - 2009 - Review of Symbolic Logic 2 (2):374-395.
On the Basic Logic of STIT with a Single Agent.Ming Xu - 1995 - Journal of Symbolic Logic 60 (2):459-483.
Decision Procedures for Some Strong Hybrid Logics.Andrzej Indrzejczak & Michał Zawidzki - 2013 - Logic and Logical Philosophy 22 (4):389-409.


Added to PP index

Total views
18 ( #515,787 of 2,289,437 )

Recent downloads (6 months)
18 ( #45,061 of 2,289,437 )

How can I increase my downloads?


My notes

Sign in to use this feature