Abstract
In this paper we present \({\mbox{\mbox{${\cal BC\!D\!L}$}}}\), a description logic based on information terms semantics, which allows a constructive interpretation of \({\mbox{\mbox{${\cal ALC}$}}}\) formulas. In the paper we describe the information terms semantics, we define a natural deduction calculus for \({\mbox{\mbox{${\cal BC\!D\!L}$}}}\) and we show it is sound and complete. As a first application of proof-theoretical properties of the calculus, we show how it fulfills the proofs-as-programs paradigm. Finally, we discuss the role of generators, the main element distinguishing our formalisation from the usual ones.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F. (eds.): The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press, Cambridge (2003)
Bozzato, L., Ferrari, M., Villa, P.: Actions over a constructive semantics for description logics. Fundam. Inform. 96, 1–17 (2009)
Brachman, R.J., Mcguinness, D.L., Patel-Schneider, P.F., Resnick, L.A., Borgida, A.: Living with CLASSIC: When and How to Use a KL-ONE-like Language (1991)
Chagrov, A., Zakharyaschev, M.: Modal Logic. Oxford University Press, Oxford (1997)
de Paiva, V.: Constructive description logics: what, why and how. Technical report, Xerox Parc (2003)
Ferrari, M., Fiorentini, C., Momigliano, A., Ornaghi, M.: Snapshot generation in a constructive object-oriented modeling language. In: King, A. (ed.) Logic Based Program Synthesis and Transformation, LOPSTR 2007, Selected Papers. Lecture Notes in Computer Science, vol. 4915, pp. 169–184. Springer, New York (2008)
Ferrari, M., Fiorentini, C., Ornaghi, M.: Extracting exact time bounds from logical proofs. In: Petterossi, A. (ed.) Logic Based Program Synthesis and Transformation, 11th International Workshop, LOPSTR 2001, Selected Papers. Lecture Notes in Computer Science, vol. 2372, pp. 245–265. Springer, New York (2002)
Gabbay, D.M.: Semantical Investigations in Heyting’s Intuitionistic Logic. Reidel, Dordrecht (1981)
Kaneiwa, K.: Negations in description logic - contraries, contradictories, and subcontraries. In: Proceedings of the 13th International Conference on Conceptual Structures (ICCS ’05), pp. 66–79. Kassel University Press, Kassel (2005)
Lipton, J., M.J. O’Donnel: Some intuitions behind realizability semantics for constructive logic: Tableaux and Läunchli countermodels. Ann. Pure Appl. Logic 81, 187–239 (1996)
Miglioli, P., Moscato, U., Ornaghi, M.: Pap: a logic programming system based on a constructive logic. In: Foundations of Logic and Functional Programming. Lecture Notes in Computer Science, vol. 306, pp. 143–156. Springer, New York (1986)
Miglioli, P., Moscato, U., Ornaghi, M.: Abstract parametric classes and abstract data types defined by classical and constructive logical methods. J. Symb. Comput. 18, 41–81 (1994)
Miglioli, P., Moscato, U., Ornaghi, M., Usberti, G.: A constructivism based on classical truth. Notre Dame J. Form. Log. 30(1), 67–90 (1989)
Nelson, D.: Constructible falsity. J. Symb. Log. 14, 16–26 (1949)
Odintsov, S.P., Wansing, H.: Inconsistency-tolerant description logic. Motivation and basic systems. In: Hendricks, V., Malinowski, J. (eds.) Trends in Logic. 50 Years of Studia Logica, pp. 301–335. Kluwer Academic, Dordrecht (2003)
Odintsov, S.P., Wansing, H.: Inconsistency-tolerant description logic. Part II: a tableau algorithm for \({{\cal CACL}}^{\mbox{c}}\). Journal of Applied Logic 6(3), 343–360 (2008)
Prawitz, D.: Natural Deduction. Almquist and Wiksell, Stockholm (1965)
Schmidt, R.A.,. Tishkovsky, D.: Using tableau to decide expressive description logics with role negation. In: ISWC/ASWC 2007. Lecture Notes in Computer Science, vol. 4825, pp. 438–451 (2007)
Schmidt-Schauß, M., Smolka, G.: Attributive concept descriptions with complements. Artif. Intell. 48(1), 1–26 (1991)
Smorynski, C.A.: Applications of Kripke semantics. In: Troelstra, A.S. (ed.) Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. Lecture Notes in Mathematics, vol. 344, pp. 324–391. Springer, New York (1973)
Troelstra, A.S. (ed.): Metamathematical Investigation of intuitionistic arithmetic and analysis. In: Lecture Notes in Mathematics, vol. 344. Springer, New York (1973)
Troelstra, A.S.: From constructivism to computer science. Theor. Comp. Sci. 211(1–2), 233–252 (1999)
Troelstra, A.S., Schwichtenberg, H.: Basic proof theory. In: Cambridge Tracts in Theoretical Computer Science, vol. 43. Cambridge University Press, Cambridge (1996)
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Ferrari, M., Fiorentini, C. & Fiorino, G. \(\boldsymbol {\cal BC\!D\!L}\): Basic Constructive Description Logic. J Autom Reasoning 44, 371–399 (2010). https://doi.org/10.1007/s10817-009-9160-7
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10817-009-9160-7