Abstract
The Ontology Web Language (OWL) is a language used for the Semantic Web. OWL is based on Description Logics (DLs), a family of logical formalisms for representing and reasoning about conceptual and terminological knowledge. Among these, the logic \(\mathcal{ALC\,}\)is a ground DL used in many practical cases. Moreover, the Semantic Web appears as a new field for the application of formal methods, that could be used to increase its reliability. A starting point could be the formal verification of satisfiability provers for DLs. In this paper, we present the PVS specification of a prover for \(\mathcal{ALC\,}\), as well as the proofs of its termination, soundness and completeness. We also present the formalization of the well–foundedness of the multiset relation induced by a well–founded relation. This result has been used to prove the termination and the completeness of the \(\mathcal{ALC\,}\) prover.
This research was partially funded by Spanish Ministry of Education and Science under grant TIN2004–03884 and Feder funds.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Aczel, P.: An introduction to inductive definitions. In: Barwise, J. (ed.) Handbook of Mathematical Logic, pp. 739–782. North–Holland Publishing Company, Amsterdam (1977)
Alonso, J.A., Borrego, J., Chávez, A.M., Martín, F.J.: Foundational challenges in automated semantic web data and ontology cleaning. IEEE Intelligent Systems 21(1), 45–52 (2006)
Alonso, J.A., Borrego, J., Hidalgo, M.J., Martín, F.J., Ruiz, J.L.: Verification of the Formal Concept Analysis. RACSAM (Revista de la Real Academia de Ciencias), Serie A: Matemáticas 98, 3–16 (2004)
Baader, F., Horrocks, I., Sattler, U.: Description logics as ontology languages for the semantic web. In: Hutter, D., Stephan, W. (eds.) Mechanizing Mathematical Reasoning. LNCS (LNAI), vol. 2605, pp. 228–248. Springer, Heidelberg (2005)
Baader, F., McGuiness, D., Nardi, D., Patel-Schneider, P. (eds.): The Description Logic Handbook: Theory, Implementation and Applications. Cambridge University Press, Cambridge (2003)
Bechhofer, S., Harmelen, F.v., Hendler, J., McGuinness, I.H.D.L., Patel-Schneider, P.F., Stein, L.A.: OWL Web Ontology Language Reference (2004), available on the Web at http://www.w3.org/TR/owl-ref
Butler, R.W., Sjogren, J.: A PVS graph theory library. Technical report, NASA Langley (1998)
Coupet-Grimal, S., Delobel, W.: An effective proof of the well–foundedness of the multiset path ordering. Applicable Algebra in Engineering, Communication and Computing 17(6), 453–469 (2006)
Dershowitz, N., Manna, Z.: Proving termination with multiset orderings. Communications of the ACM 22(8), 465–476 (1979)
Haarslev, V., Möller, R.: RACER system description. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, pp. 701–705. Springer, Heidelberg (2001)
Harrison, J.: Formalizing basic first order model theory. In: Grundy, J., Newey, M. (eds.) Theorem Proving in Higher Order Logics. LNCS, vol. 1479, Springer, Heidelberg (1998)
Horrocks, I., Patel-Schneider, P.: Reducing OWL entailment to description logic satisfiability. J. of Web Semantics 1(4), 345–357 (2004)
Horrocks, I., Patel-Schneider, P.F., van Harmelen, F.: From \(\mathcal{SHIQ}\) and RDF to OWL: The making of a Web Ontology Language. J. of Web Semantics 1(1), 7–26 (2003)
Martín, F.J., Alonso, J.A., Hidalgo, M.J., Ruiz, J.L.: Formal verification of a generic framework to synthesize SAT–provers. Journal of Automated Reasoning 32(4), 287–313 (2004)
Medina, I., Palomo, F., Alonso, J.A.: A certified polynomial-based decision procedure for propositional logic. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol. 2152, pp. 297–312. Springer, Heidelberg (2001)
Medina, I., Palomo, F., Alonso, J.A., Ruiz, J.L.: Verified computer algebra in ACL2. In: Buchberger, B., Campbell, J.A. (eds.) AISC 2004. LNCS (LNAI), vol. 3249, pp. 171–184. Springer, Heidelberg (2004)
Nipkow, T.: An inductive proof of the wellfoundedness of the multiset order. A proof due to W. Buchholz (1998), available on the Web at http://www4.informatik.tu-muenchen.de/~nipkow/misc/multiset.ps
Nutt, W.: Algorithms for constraint in deduction and knowledge representation. PhD thesis, Universität des Saarlandes (1993)
Owre, S., Rushby, J.M., Shankar, N.: PVS: A Prototype Verification System. In: Kapur, D. (ed.) Automated Deduction - CADE-11. LNCS, vol. 607, pp. 748–752. Springer, Heidelberg (1992)
Owre, S., Shankar, N.: Abstract datatype in PVS. Technical report, Computer Science Laboratory, SRI International (1997)
Ridge, T., Margetson, J.: A mechanically verified, sound and complete theorem prover for first order logic. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 294–309. Springer, Heidelberg (2005)
Ruiz, J.L., Alonso, J.A., Hidalgo, M.J., Martín, F.J.: Formal proofs about rewriting using ACL2. Ann. Math. Artif. Intell. 36(3), 239–262 (2002)
Ruiz, J.L., Alonso, J.A., Hidalgo, M.J., Martín, F.J.: Termination in ACL2 using multiset relation. In: Kamareddine, F.D. (ed.) Thirty Five Years of Automating Mathematics, pp. 217–245. Kluwer Academic Publishers, Dordrecht (2003)
Schmidt–Schauß, M., Smolka, G.: Attributive concept descriptions with complements. Artificial Intelligence 48(1), 1–26 (1991)
Tsarkov, D., Horrocks, I.: FaCT++ description logic reasoner: System description. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 292–297. Springer, Heidelberg (2006)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Alonso, JA., Borrego-Díaz, J., Hidalgo, MJ., Martín-Mateos, FJ., Ruiz-Reina, JL. (2007). A Formally Verified Prover for the \(\mathcal{ALC\,}\) Description Logic. In: Schneider, K., Brandt, J. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2007. Lecture Notes in Computer Science, vol 4732. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74591-4_11
Download citation
DOI: https://doi.org/10.1007/978-3-540-74591-4_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-74590-7
Online ISBN: 978-3-540-74591-4
eBook Packages: Computer ScienceComputer Science (R0)