Skip to main content

Tableaux and Complexity Bounds for a Multiagent Justification Logic with Interacting Justifications

  • Conference paper
  • First Online:
Multi-Agent Systems (EUMAS 2014)

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

Included in the following conference series:

Abstract

We introduce a family of multi-agent justification logics with interactions between the agents’ justifications, by extending and generalizing the two-agent versions of the Logic of Proofs (LP) introduced by Yavorskaya in 2008. LP, and its successor, Justification Logic, is a refinement of the modal logic approach to epistemology in which for every belief assertion, an explicit justification is supplied. This affects the complexity of the logic’s derivability problem, which is known to be in the second level of the polynomial hierarchy (first result by Kuznets in 2000) for all single-agent justification logics whose complexity is known. We present tableau rules and some complexity results. In several cases the satisfiability problem for these logics remains in the second level of the polynomial hierarchy, while the problem becomes PSPACE-hard for certain two-agent logics and there are EXP-hard logics of three agents.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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

Institutional subscriptions

Notes

  1. 1.

    Thus, if \(i\) has positive introspection (i.e. \(i \hookrightarrow i\)), then \(R_i\) is transitive.

  2. 2.

    That \(\mathcal {CS}\) is axiomatically appropriate is a requirement for completeness.

  3. 3.

    In fact, it is not hard to demonstrate how to construct from a model \(\mathcal {M}= (W,(R_i)_{i\in [n]},{\mathcal {E}},\mathcal {V})\) a model \(\mathcal {M}' = (W,(R_i)_{i\in [n]},{\mathcal {E}}',\mathcal {V})\) which has the Strong Evidence Property and for every \(w \in W\) and \(\phi \in L_n\), \(\mathcal {M},w\,{\models }\,\phi \) iff \(\mathcal {M}',w\,{\models }\,\phi \): just define \({\mathcal {E}}_i(t,\phi ) = \{w \in W \mid \mathcal {M},w\,{\models }\,t\! :_{i} \!\phi \}\).

  4. 4.

    \(\mathcal {J}_{1}\) would correspond to what is defined in [3] as \(\mathsf{D}_2 \oplus _\subseteq \mathsf{K}\) and \(\mathcal {J}_{2}\) to \(\mathsf{D}_2 \oplus _\subseteq \mathsf{D4}\). Then we can pick a justification variable \(x\) and we can either use the same reductions and substitute \(\Box _i\) by \(x\! :_{i} \!\), or we can just translate each diamond-free fragment to the corresponding justification logic in the same way. It is not hard to see then that the original modal formula behaves exactly the same way as the result of its translation with respect to satisfiability – just consider F-models where always \({\mathcal {E}}_i(t,\phi ) = W\).

References

  1. Achilleos, A.: A complexity question in justification logic. J. Comput. Syst. Sci. 80(6), 1038–1045 (2014)

    Article  MATH  MathSciNet  Google Scholar 

  2. Achilleos, A.: Modal logics with hard diamond-free fragments. CoRR, abs/1401.5846 (2014)

    Google Scholar 

  3. Achilleos, A.: On the complexity of two-agent justification logic. In: Bulling, N., van der Torre, L., Villata, S., Jamroga, W., Vasconcelos, W. (eds.) CLIMA 2014. LNCS, vol. 8624, pp. 1–18. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  4. Artemov, S.: Explicit provability and constructive semantics. Bull. Symbolic Logic 7(1), 1–36 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  5. Artemov, S.: Justification logic. In: Hölldobler, S., Lutz, C., Wansing, H. (eds.) JELIA 2008. LNCS (LNAI), vol. 5293, pp. 1–4. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  6. Artemov, S.: The logic of justification. Rev. Symbolic Logic 1(4), 477–513 (2008)

    Article  MATH  Google Scholar 

  7. Artemov, S., Kuznets, R.: Logical omniscience as infeasibility. Ann. Pure Appl. Logic 165(1), 6–25 (2014). http://dx.doi.org/10.1016/j.apal.2013.07.003

    Article  MATH  MathSciNet  Google Scholar 

  8. Buss, S.R., Kuznets, R.: Lower complexity bounds in justification logic. Ann. Pure Appl. Logic 163(7), 888–905 (2012)

    Article  MATH  MathSciNet  Google Scholar 

  9. Demri, S.: Complexity of simple dependent bimodal logics. In: Dyckhoff, R. (ed.) TABLEAUX 2000. LNCS, vol. 1847, pp. 190–204. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  10. Dziubiński, M., Verbrugge, R., Dunin-Kȩplicz, B.: Complexity issues in multiagent logics. Fundamenta Informaticae 75(1), 239–262 (2007)

    MATH  MathSciNet  Google Scholar 

  11. Fitting, M.: The logic of proofs, semantically. Ann. Pure Appl. Logic 132(1), 1–25 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  12. Krupski, N.V.: On the complexity of the reflected logic of proofs. Theor. Comput. Sci. 357(1–3), 136–142 (2006)

    Article  MATH  MathSciNet  Google Scholar 

  13. Kuznets, R.: On the complexity of explicit modal logics. In: Clote, P.G., Schwichtenberg, H. (eds.) CSL 2000. LNCS, vol. 1862, pp. 371–383. Springer, Heidelberg (2000). Errata concerning the explicit counterparts of \({\cal D}\) and \({\cal D4}\) are published as [15]

    Chapter  Google Scholar 

  14. Kuznets, R.: Complexity Issues in Justification Logic. Ph.D. thesis, CUNY Graduate Center, May 2008

    Google Scholar 

  15. Kuznets, R.: Complexity through tableaux in justification logic. In: Plenary Talks, Tutorials, Special Sessions, Contributed Talks of Logic Colloquium (LC 2008), Bern, Switzerland, pp. 38–39 (2008)

    Google Scholar 

  16. Kuznets, R.: Self-referentiality of justified knowledge. In: Hirsch, E.A., Razborov, A.A., Semenov, A., Slissenko, A. (eds.) Computer Science – Theory and Applications. LNCS, vol. 5010, pp. 228–239. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  17. Kuznets, R., Studer, T.: Update as evidence: belief expansion. In: Artemov, S., Nerode, A. (eds.) LFCS 2013. LNCS, vol. 7734, pp. 266–279. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  18. Mkrtychev, A.: Models for the logic of proofs. In: Adian, S., Nerode, A. (eds.) Logical Foundations of Computer Science. LNCS, vol. 1234, pp. 266–275. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  19. Pacuit, E.: A note on some explicit modal logics. In: Proceedings of the 5th Panhellenic Logic Symposium, Athens, Greece, University of Athens (2005)

    Google Scholar 

  20. Spaan, E.: Complexity of modal logics. Ph.D. thesis, University of Amsterdam (1993)

    Google Scholar 

  21. Yavorskaya (Sidon), T.: Interacting explicit evidence systems. Theor. Comput. Syst. 43(2), 272–293 (2008)

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Antonis Achilleos .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Achilleos, A. (2015). Tableaux and Complexity Bounds for a Multiagent Justification Logic with Interacting Justifications. In: Bulling, N. (eds) Multi-Agent Systems. EUMAS 2014. Lecture Notes in Computer Science(), vol 8953. Springer, Cham. https://doi.org/10.1007/978-3-319-17130-2_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-17130-2_12

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-17129-6

  • Online ISBN: 978-3-319-17130-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics