Reasoning with Justifications

  • Melvin FittingEmail author
Part of the Trends in Logic book series (TREN, volume 28)


This is an expository paper in which the basic ideas of a family of Justification Logics are presented. Justification Logics evolved from a logic called \(\mathsf{LP}\) , introduced by Sergei Artemov (Technical Report MSI 95-29, 1995; The Bulletin for Symbolic Logic 7(1): 1–36, 2001), which formed the central part of a project to provide an arithmetic semantics for propositional intuitionistic logic. The project was successful, but there was a considerable bonus: \(\mathsf{LP}\) came to be understood as a logic of knowledge with explicit justifications and, as such, was capable of addressing in a natural way long-standing problems of logical omniscience. Since then, \(\mathsf{LP}\) has become one member of a family of related logics, all logics of knowledge with explicit knowledge terms. In this paper the original problem of intuitionistic foundations is discussed only briefly. We concentrate entirely on issues of reasoning about knowledge.


logic of knowledge justification logic modal logic 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    Artemov, S., Operational modal logic, Technical Report MSI 95-29, Cornell University, December 1995. Google Scholar
  2. [2]
    Artemov, S., Logic of proofs: a unified semantics for modality and lambda-terms, Technical Report CFIS 98-17, Cornell University, 1998. Google Scholar
  3. [3]
    Artemov, S., ‘Explicit provability and constructive semantics’, The Bulletin for Symbolic Logic, 7(1): 1–36, 2001. zbMATHCrossRefMathSciNetGoogle Scholar
  4. [4]
    Artemov, S., Evidence-based common knowledge, Technical Report TR-2004018, CUNY Ph.D. Program in Computer Science, 2004. Google Scholar
  5. [5]
    Artemov, S., ‘Justified common knowledge’, Theoretical Computer Science, 357(1–3): 4–22, 2006. zbMATHCrossRefMathSciNetGoogle Scholar
  6. [6]
    Artemov, S., Kazakov, E., Shapiro, D., On logic of knowledge with justifications, Technical Report CFIS 99-12, Cornell University, 1999. Google Scholar
  7. [7]
    Artemov, S., Kuznets, R., ‘Logical omniscience via proof complexity’, in Computer Science Logic 2006, Lecture Notes in Computer Science, vol. 4207, Springer, Berlin, 2006, pp. 135–149. CrossRefGoogle Scholar
  8. [8]
    Artemov, S., Nogina, E., ‘Introducing justification into epistemic logic’, Journal of Logic and Computation, 15(6): 1059–1073, 2005. zbMATHCrossRefMathSciNetGoogle Scholar
  9. [9]
    Brezhnev, V., ‘On the logic of proofs’, in Striegnitz, K. (ed.), Proceedings of the Sixth ESSLLI Student Session, Helsinki, 2001, pp. 35–46. Google Scholar
  10. [10]
    Brezhnev, V., Kuznets, R., ‘Making knowledge explicit: How hard it is’, Theoretical Computer Science, 357: 23–34, 2006. zbMATHCrossRefMathSciNetGoogle Scholar
  11. [11]
    Fagin, R., Halpern, J.Y., ‘Beliefs, awareness and limited reasoning’, Artificial Intelligence, 34: 39–76, 1988. CrossRefMathSciNetGoogle Scholar
  12. [12]
    Feferman, S. (ed.), Kurt Gödel Collected Works, Oxford, 1986–2003. Five volumes. Google Scholar
  13. [13]
    Fitting, M.C., ‘The logic of proofs, semantically’, Annals of Pure and Applied Logic, 132: 1–25, 2005. zbMATHCrossRefMathSciNetGoogle Scholar
  14. [14]
    Fitting, M.C., ‘A quantified logic of evidence (short version)’, in de Queiroz, R., Macintyre, A. Bittencourt, G. (eds.), WoLLIC 2005 Proceedings, Electronic Notes in Theoretical Computer Science, Elsevier, Amsterdam, 2005, pp. 59–70. Google Scholar
  15. [15]
    Fitting, M.C., Realizations and LP. Available at, 2006. Google Scholar
  16. [16]
    Fitting, M.C., Realizing substitution instances of modal theorems. Available at, 2006. Google Scholar
  17. [17]
    Fitting, M.C., A replacement theorem for LP, Technical report, CUNY Ph.D. Program in Computer Science, 2006. Google Scholar
  18. [18]
    Fitting, M.C., ‘A quantified logic of evidence’, Annals of Pure and Applied Logic, 2007. Forthcoming. Google Scholar
  19. [19]
    Gödel, K., ‘Eine Interpretation des intuistionistischen Aussagenkalkuls’, Ergebnisse eines mathematischen Kolloquiums, 4: 39–40, 1933. Translated as ‘An interpretation of the intuitionistic propositional calculus’, in [12] 296–301. Google Scholar
  20. [20]
    Gödel, K., ‘Vortrag bei Zilsel’. Translated as ‘Lecture at Zilsel’s’, in Feferman, S. (ed.), Kurt Gödel Collected Works, Oxford, 1986–2003. Five volumes. III, 62–113, 1938. Google Scholar
  21. [21]
    Hintikka, J., Knowledge and Belief, Cornell University Press, Ithaca, NY, 1962. Google Scholar
  22. [22]
    Mkrtychev, A., ‘Models for the logic of proofs’, in Adian, S.I., Nerode, A. (eds.), Logical Foundations of Computer Science, Lecture Notes in Computer Science, vol. 1234, Springer, Berlin, 1997, pp. 266–275. Google Scholar
  23. [23]
    Pacuit, E., ‘A note on some explicit modal logics’, in Acopoulos, C. Dimitr (ed.), Proceedings of the Fifth Panhellenic Logic Symposium, 2005, pp. 117–125. Google Scholar
  24. [24]
    Renne, B., ‘Bisimulation and public announcements in logics of explicit knowledge’, in Artemov, S., Parikh, R. (eds.), Proceedings of the Workshop on Rationality and Knowledge, 18th European Summer School in Logic, Language, and Information (ESSLLI), Málaga, Spain, 2006, pp. 112–123. Google Scholar
  25. [25]
    Rubtsova, N., ‘Evidence reconstruction of epistemic modal logic S5’, in Grigoriev, D., Harrison, J., Hirsch, E.A. (eds.), Computer Science—Theory and Applications, Lecture Notes in Computer Science, vol. 3967, Springer-Verlag, Berlin, 2006, pp. 313–321. Google Scholar
  26. [26]
    Yavorskaya, T. (Sidon), ‘Logic of proofs with two proof predicates’, in Grivoriev, D., Harrison, J., Hirsch, E. (eds.), Computer Science—Theory and Applications, Lecture Notes in Computer Science, vol. 3967, Springer, Berlin, 2006. Google Scholar
  27. [27]
    Yavorsky, R., ‘Provability logics with quantifiers on proofs’, Annals of Pure and Applied Logic, 113(1–3): 373–387, 2002. zbMATHMathSciNetGoogle Scholar

Copyright information

© Springer Science+Business Media B.V. 2009

Authors and Affiliations

  1. 1.Department of Computer ScienceThe Graduate School & University Center, CUNYNew York CityUSA

Personalised recommendations