Abstract
This work provides proof-search algorithms and automated counter-model extraction for a class of \(\mathsf {STIT}\) logics. With this, we answer an open problem concerning syntactic decision procedures and cut-free calculi for \(\mathsf {STIT}\) logics. A new class of cut-free complete labelled sequent calculi \(\mathsf {G3Ldm}_{n}^{m}\), for multi-agent \(\mathsf {STIT}\) with at most n-many choices, is introduced. We refine the calculi \(\mathsf {G3Ldm}_{n}^{m}\) through the use of propagation rules and demonstrate the admissibility of their structural rules, resulting in the auxiliary calculi \(\mathsf {Ldm}_{n}^{m}\mathsf {L}\). In the single-agent case, we show that the refined calculi \(\mathsf {Ldm}_{n}^{m}\mathsf {L}\) derive theorems within a restricted class of (forestlike) sequents, allowing us to provide proof-search algorithms that decide single-agent \(\mathsf {STIT}\) logics. We prove that the proof-search algorithms are correct and terminate.
Work funded by the projects WWTF MA16-028, FWF I2982 and FWF W1255-N23.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
For a discussion of the philosophical utility of reasoning with limited choice see [20].
- 2.
For further information on regular languages and expressions, consult [16].
- 3.
Observe that \(\mathcal {P}_{\varLambda _{1}}(w,u) = \mathcal {P}_{\varLambda _{2}}(w,u)\). Hence, deciding which automaton to employ in determining the side condition is inconsequential: when applying the rule top-down we may consult \(\varLambda _1\), whereas during bottom-up proof-search we may regard \(\varLambda _2\).
References
Arkoudas, K., Bringsjord S., Bello, P.: Toward ethical robots via mechanized deontic logic. In: AAAI Fall Symposium on Machine Ethics, pp. 17–23 (2005)
Balbiani, P., Herzig, A., Troquard, N.: Alternative axiomatics and complexity of deliberative STIT theories. J. Philos. Logic 37(4), 387–406 (2008)
Belnap, N., Perloff, M., Xu, M.: Facing the Future: Agents and Choices in Our Indeterminist World. Oxford University Press on Demand, Oxford (2001)
van Berkel, K., Lyon, T.: Cut-free calculi and relational semantics for temporal STIT logics. In: Calimeri, F., Leone, N., Manna, M. (eds.) JELIA 2019. LNCS (LNAI), vol. 11468, pp. 803–819. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-19570-0_52
Broersen, J.: Deontic epistemic stit logic distinguishing modes of mens rea. J. Appl. Logic 9(2), 137–152 (2011)
Ciabattoni, A., Lyon, T., Ramanayake, R.: From display to labelled proofs for tense logics. In: Artemov, S., Nerode, A. (eds.) LFCS 2018. LNCS, vol. 10703, pp. 120–139. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-72056-2_8
Gentzen, G.: Untersuchungen über das logische Schließen. Math. Z. 39(3), 405–431 (1935)
Girlando, M., Lellmann, B., Olivetti, N., Pozzato, G.L., Vitalis, Q.: VINTE: an implementation of internal calculi for lewis’ logics of counterfactual reasoning. In: Schmidt, R.A., Nalon, C. (eds.) TABLEAUX 2017. LNCS (LNAI), vol. 10501, pp. 149–159. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66902-1_9
Grossi, D., Lorini, E., Schwarzentruber, F.: The ceteris paribus structure of logics of game forms. J. Artif. Intell. Res. 53, 91–126 (2015)
Herzig, A., Schwarzentruber, F.: Properties of logics of individual and group agency. Adv. Modal Logic 7, 133–149 (2008)
Horty, J.: Agency and Deontic Logic. Oxford University Press, Oxford (2001)
Lorini, E., Sartor, G.: Influence and responsibility: a logical analysis. In: Legal Knowledge and Information Systems, pp. 51–60. IOS Press (2015)
Murakami, Y.: Utilitarian deontic logic. Adv. Modal Logic 5, 211–230 (2005)
Negri, S.: Proof analysis in modal logic. J. Philos. Logic 34(5–6), 507–544 (2005)
Schwarzentruber, F.: Complexity results of stit fragments. Stud. Logica 100(5), 1001–1045 (2012)
Sipser, M.: Introduction to the Theory of Computation. Course Technology (2006)
Tiu, A., Ianovski, E., Goré, R.: Grammar Logics in Nested Sequent Calculus: Proof Theory and Decision Procedures. CoRR (2012)
Viganò, L.: Labelled Non-classical Logics. Kluwer Academic Publishers, Dordrecht (2000)
Wansing, H.: Tableaux for multi-agent deliberative-stit logic. Adv. Modal Logic 6, 503–520 (2006)
Xu, M.: Decidability of deliberative stit theories with multiple agents. In: Gabbay, D.M., Ohlbach, H.J. (eds.) ICTL 1994. LNCS, vol. 827, pp. 332–348. Springer, Heidelberg (1994). https://doi.org/10.1007/BFb0013997
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Lyon, T., van Berkel, K. (2019). Automating Agential Reasoning: Proof-Calculi and Syntactic Decidability for STIT Logics. In: Baldoni, M., Dastani, M., Liao, B., Sakurai, Y., Zalila Wenkstern, R. (eds) PRIMA 2019: Principles and Practice of Multi-Agent Systems. PRIMA 2019. Lecture Notes in Computer Science(), vol 11873. Springer, Cham. https://doi.org/10.1007/978-3-030-33792-6_13
Download citation
DOI: https://doi.org/10.1007/978-3-030-33792-6_13
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-33791-9
Online ISBN: 978-3-030-33792-6
eBook Packages: Computer ScienceComputer Science (R0)