Skip to main content
SpringerLink
Log in
Book cover

International Conference on Principles and Practice of Multi-Agent Systems

PRIMA 2019: PRIMA 2019: Principles and Practice of Multi-Agent Systems pp 202–218Cite as

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

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 11873))

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.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   84.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    For a discussion of the philosophical utility of reasoning with limited choice see [20].

  2. 2.

    For further information on regular languages and expressions, consult [16].

  3. 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

  1. Arkoudas, K., Bringsjord S., Bello, P.: Toward ethical robots via mechanized deontic logic. In: AAAI Fall Symposium on Machine Ethics, pp. 17–23 (2005)

    Google Scholar 

  2. Balbiani, P., Herzig, A., Troquard, N.: Alternative axiomatics and complexity of deliberative STIT theories. J. Philos. Logic 37(4), 387–406 (2008)

    Article  MathSciNet  Google Scholar 

  3. Belnap, N., Perloff, M., Xu, M.: Facing the Future: Agents and Choices in Our Indeterminist World. Oxford University Press on Demand, Oxford (2001)

    Google Scholar 

  4. 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

    Chapter  Google Scholar 

  5. Broersen, J.: Deontic epistemic stit logic distinguishing modes of mens rea. J. Appl. Logic 9(2), 137–152 (2011)

    Article  MathSciNet  Google Scholar 

  6. 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

    Chapter  Google Scholar 

  7. Gentzen, G.: Untersuchungen über das logische Schließen. Math. Z. 39(3), 405–431 (1935)

    Article  MathSciNet  Google Scholar 

  8. 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

    Chapter  MATH  Google Scholar 

  9. Grossi, D., Lorini, E., Schwarzentruber, F.: The ceteris paribus structure of logics of game forms. J. Artif. Intell. Res. 53, 91–126 (2015)

    Article  MathSciNet  Google Scholar 

  10. Herzig, A., Schwarzentruber, F.: Properties of logics of individual and group agency. Adv. Modal Logic 7, 133–149 (2008)

    MathSciNet  MATH  Google Scholar 

  11. Horty, J.: Agency and Deontic Logic. Oxford University Press, Oxford (2001)

    Book  Google Scholar 

  12. Lorini, E., Sartor, G.: Influence and responsibility: a logical analysis. In: Legal Knowledge and Information Systems, pp. 51–60. IOS Press (2015)

    Google Scholar 

  13. Murakami, Y.: Utilitarian deontic logic. Adv. Modal Logic 5, 211–230 (2005)

    MathSciNet  MATH  Google Scholar 

  14. Negri, S.: Proof analysis in modal logic. J. Philos. Logic 34(5–6), 507–544 (2005)

    Article  MathSciNet  Google Scholar 

  15. Schwarzentruber, F.: Complexity results of stit fragments. Stud. Logica 100(5), 1001–1045 (2012)

    Article  MathSciNet  Google Scholar 

  16. Sipser, M.: Introduction to the Theory of Computation. Course Technology (2006)

    Google Scholar 

  17. Tiu, A., Ianovski, E., Goré, R.: Grammar Logics in Nested Sequent Calculus: Proof Theory and Decision Procedures. CoRR (2012)

    Google Scholar 

  18. Viganò, L.: Labelled Non-classical Logics. Kluwer Academic Publishers, Dordrecht (2000)

    Book  Google Scholar 

  19. Wansing, H.: Tableaux for multi-agent deliberative-stit logic. Adv. Modal Logic 6, 503–520 (2006)

    MathSciNet  MATH  Google Scholar 

  20. 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

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Logic and Computation, Technische Universität Wien, 1040, Wien, Austria

    Tim Lyon & Kees van Berkel

Authors
  1. Tim Lyon
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Kees van Berkel
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Tim Lyon .

Editor information

Editors and Affiliations

  1. Università degli Studi di Torino, Turin, Italy

    Matteo Baldoni

  2. Utrecht University, Utrecht, The Netherlands

    Mehdi Dastani

  3. Zhejiang University, Hangzhou, China

    Beishui Liao

  4. National Institute of Advanced Industrial Science and Technology, Tokyo, Japan

    Yuko Sakurai

  5. University of Texas at Dallas, Richardson, TX, USA

    Rym Zalila Wenkstern

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

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)

Publish with us

Policies and ethics

Search

Navigation