On the Sharpness and the Single-Conclusion Property of Basic Justification Models

  • Vladimir N. KrupskiEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10703)


Justification Awareness Models, JAMs, were proposed by S. Artemov as a tool for modelling epistemic scenarios like Russell’s Prime Minister example. It was demonstrated that the sharpness and the single-conclusion property of a model play essential role in the epistemic usage of JAMs. The problem to axiomatize these properties using the propositional justification language was left opened. We propose the solution and define a decidable justification logic \(\mathsf{J}_{\text{ref}}\) that is sound and complete with respect to the class of all sharp single-conclusion justification models.


Modal logic Justification logic Justification awareness models Single-conclusion property Sharpness property 



I would like to thank Sergei Artemov who attracted my attention to the problem.


  1. 1.
    Artemov, S., Straßen, T.: Functionality in the basic logic of proofs. Technical report IAM 92–004, University of Bern (1993)Google Scholar
  2. 2.
    Artemov, S.: The logic of justification. Rev. Symb. Log. 1(4), 477–513 (2008)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Artemov, S.: Epistemic Modeling with Justifications. arXiv:1703.07028v1 (2017)
  4. 4.
    Artemov, S.: Justification awareness models. In: Artemov, S., Nerode, A. (eds.) LFCS 2018. LNCS, vol. 10703, pp. 22–36. Springer, Cham (2018)Google Scholar
  5. 5.
    Farmer, W.M.: Simple second-order languages for which unification is undecidable. Theor. Comput. Sci. 87, 25–41 (1991)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Goldfarb, W.G.: The undecidability of the second-order unification problem. Theor. Comput. Sci. 13, 225–230 (1981)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Krupski, V.N.: Operational logic of proofs with functionality condition on proof predicate. In: Adian, S., Nerode, A. (eds.) Logical Foundations of Computer Science 1997. LNCS, vol. 1234, pp. 167–177. Springer, Heidelberg (1997)Google Scholar
  8. 8.
    Krupski, V.N.: The single-conclusion proof logic and inference rules specification. Ann. Pure Appl. Log. 113(1–3), 181–206 (2001)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Krupski, V.N.: Reference constructions in the single-conclusion proof logic. J. Log. Comput. 16(5), 645–661 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    Krupski, V.N.: Referential logic of proofs. Theor. Comput. Sci. 357, 143–199 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Krupski, V.N.: Symbolic models for single-conclusion proof logics. In: Ablayev, F., Mayr, E.W. (eds.) CSR 2010. LNCS, vol. 6072, pp. 276–287. Springer, Heidelberg (2010). CrossRefGoogle Scholar
  12. 12.
    Krupski, V.N.: On symbolic models for single-conclusion logic of proofs. Sb. Math. 202(5), 683–695 (2011)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer International Publishing AG 2018

Authors and Affiliations

  1. 1.Faculty of Mechanics and MathematicsLomonosov Moscow State UniversityMoscowRussia

Personalised recommendations