Justification logics are epistemic logics that include explicit justifications for an agent’s knowledge. In the present paper, we introduce a justification logic \(\mathcal{JALC}\) over the description logic \(\mathcal{ALC}\). We provide a deductive system and a semantics for our logic and we establish soundness and completeness results. Moreover, we show that our logic satisfies the so-called internalization property stating that it internalizes its own notion of proof. We then sketch two applications of \(\mathcal{JALC}\): (i) the justification terms can be used to generate natural language explanations why an \(\mathcal{ALC}\) statement holds and (ii) the terms can be used to study data privacy issues for description logic knowledge bases.


Justification logic description logic inference tracking explanations data privacy 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Angele, J., Moench, E., Oppermann, H., Staab, S., Wenke, D.: Ontology-based query and answering in chemistry: OntoNova @ project halo. In: Proc. of the 2nd Int. Semantic Web Conference ISWC (1993)Google Scholar
  2. 2.
    Artemov, S.N.: Operational modal logic. Technical Report MSI 95–29, Cornell University (December 1995)Google Scholar
  3. 3.
    Artemov, S.N.: Explicit provability and constructive semantics. Bulletin of Symbolic Logic 7(1), 1–36 (2001)MathSciNetzbMATHCrossRefGoogle Scholar
  4. 4.
    Artemov, S.N.: The logic of justification. The Review of Symbolic Logic 1(4), 477–513 (2008)zbMATHCrossRefGoogle Scholar
  5. 5.
    Artemov, S.: Tracking Evidence. In: Blass, A., Dershowitz, N., Reisig, W. (eds.) Fields of Logic and Computation. LNCS, vol. 6300, pp. 61–74. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  6. 6.
    Artemov, S.N., Kuznets, R.: Logical omniscience as a computational complexity problem. In: Heifetz, A. (ed.) Theoretical Aspects of Rationality and Knowledge, Proceedings of the Twelfth Conference (TARK 2009), Stanford University, California, July 6-8, pp. 14–23. ACM (2009)Google Scholar
  7. 7.
    Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F. (eds.): The Description Logic Handbook, 2nd edn. Cambridge University Press (2007)Google Scholar
  8. 8.
    Baader, F., Laux, A.: Terminological logics with modal operators. In: Proc. of IJCAI 1995, pp. 808–814. Morgan Kaufmann (1995)Google Scholar
  9. 9.
    Bao, J., Slutzki, G., Honavar, V.: Privacy-preserving reasoning on the semantic web. In: Web Intelligence 2007, pp. 791–797 (2007)Google Scholar
  10. 10.
    Bucheli, S., Kuznets, R., Renne, B., Sack, J., Studer, T.: Justified belief change. In: Arrazola, X., Ponte, M. (eds.) LogKCA 2010, Proceedings of the Second ILCLI International Workshop on Logic and Philosophy of Knowledge, Communication and Action, pp. 135–155. University of the Basque Country Press (2010)Google Scholar
  11. 11.
    Bucheli, S., Kuznets, R., Studer, T.: Partial Realization in Dynamic Justification Logic. In: Beklemishev, L.D., de Queiroz, R. (eds.) WoLLIC 2011. LNCS, vol. 6642, pp. 35–51. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  12. 12.
    Calvanese, D., De Giacomo, G., Lenzerini, M., Rosati, R.: View-based query answering over description logic ontologies. In: Principles of Knowledge Representation and Reasoning, pp. 242–251 (2008)Google Scholar
  13. 13.
    Cuenca Grau, B., Horrocks, I.: Privacy-preserving query answering in logic-based information systems. In: ECAI 2008 (2008)Google Scholar
  14. 14.
    Donini, F., Lenzerini, M., Nardi, D., Nutt, W., Schaerf, A.: An epistemic operator for escription logics. Artificial Intelligence 100(1-2), 225–274 (1998)MathSciNetzbMATHCrossRefGoogle Scholar
  15. 15.
    Finger, M., Gabbay, D.: Adding a temporal dimension to a logic system. Journal of Logic Language and Information 1, 203–233 (1992)MathSciNetzbMATHCrossRefGoogle Scholar
  16. 16.
    Fitting, M.: The logic of proofs, semantically. Annals of Pure and Applied Logic 132(1), 1–25 (2005)MathSciNetzbMATHCrossRefGoogle Scholar
  17. 17.
    Gräber, A., Bürckert, H., Laux, A.: Terminological reasoning with knowledge and belief. In: Knowledge and Belief in Philosophy and Artificial Intelligence, pp. 29–61. Akademie Verlag (1995)Google Scholar
  18. 18.
    Kuznets, R.: Self-referential justifications in epistemic logic. Theory of Computing Systems 46(4), 636–661 (2010)MathSciNetzbMATHCrossRefGoogle Scholar
  19. 19.
    Laux, A.: Beliefs in multi-agent worlds: a terminological approach. In: Proc. of ECAI 1994, pp. 299–303 (1994)Google Scholar
  20. 20.
    Lutz, C., Sturm, H., Wolter, F., Zakharyaschev, M.: A tableau decision algorithm for modalized ALC with constant domains. Studia Logica 72, 199–232 (2002)MathSciNetzbMATHCrossRefGoogle Scholar
  21. 21.
    McGuiness, D., Pinheiro da Silva, P.: Inference web: Portable and shareable explanations for question answering. In: Proc. of AAAI Workshop on New Directions for Question Answering (1993)Google Scholar
  22. 22.
    Schild, K.: A correspondence theory for terminological logics: Preliminary report. In: Proc. of IJCAI, pp. 466–471 (1991)Google Scholar
  23. 23.
    Stouppa, P., Studer, T.: Data Privacy for \(\mathcal{ALC}\) Knowledge Bases. In: Artemov, S., Nerode, A. (eds.) LFCS 2009. LNCS, vol. 5407, pp. 409–421. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  24. 24.
    Studer, T.: Privacy Preserving Modules for Ontologies. In: Pnueli, A., Virbitskaite, I., Voronkov, A. (eds.) PSI 2009. LNCS, vol. 5947, pp. 380–387. Springer, Heidelberg (2010)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Thomas Studer
    • 1
  1. 1.Institut für Informatik und angewandte MathematikUniversität BernSwizerland

Personalised recommendations