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

Tim LyonTim Lyon, Kees van BerkelKees van Berkel

ISBN: 978-3-030-33792-6
Download
DOI Link

Tim Lyon, Kees van Berkel
Automating Agential Reasoning: Proof-Calculi and Syntactic Decidability for STIT Logics
In Baldoni, Matteo and Dastani, Mehdi and Liao, Beishui and Sakurai, Yuko and Zalila Wenkstern, Rym, eds., PRIMA 2019: Principles and Practice of Multi-Agent Systems, volume 11873, 202-218, 2019. Springer

Details
Bibtex

KurzfassungAbstract
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.
Weitere Informationen unter:Further Information: Link
Forschungsgruppe:Research Group: Computational LogicComputational Logic

The final publication is available at Springer via http://dx.doi.org/https://doi.org/10.1007/978-3-030-33792-6_13.

@InProceedings{10.1007/978-3-030-33792-6_13,
author="Lyon, Tim
and van Berkel, Kees",
editor="Baldoni, Matteo
and Dastani, Mehdi
and Liao, Beishui
and Sakurai, Yuko
and Zalila Wenkstern, Rym",
title="Automating Agential Reasoning: Proof-Calculi and Syntactic Decidability for STIT Logics",
booktitle="PRIMA 2019:  Principles and Practice of Multi-Agent Systems",
year="2019",
publisher="Springer International Publishing",
address="Cham",
pages="202--218",
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.",
isbn="978-3-030-33792-6"
}