Repositorio de producción científica de la Universidad de Sevilla

A Formally Verified Prover for the ALC Description Logic

 

Advanced Search
 
Opened Access A Formally Verified Prover for the ALC Description Logic
Cites

Show item statistics
Icon
Export to
Author: Alonso Jiménez, José Antonio
Borrego Díaz, Joaquín
Hidalgo Doblado, María José
Martín Mateos, Francisco Jesús
Ruiz Reina, José Luis
Department: Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial
Date: 2007
Published in: TPHOLs 2007: 20th International Conference on Theorem Proving in Higher Order Logics (2007), p 135-150
ISBN/ISSN: 978-3-540-74590-7
0302-9743
Document type: Presentation
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 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 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 ALC prover.
Cite: Alonso Jiménez, J.A., Borrego Díaz, J., Hidalgo Doblado, M.J., Martín Mateos, F.J. y Ruiz Reina, J.L. (2007). A Formally Verified Prover for the ALC Description Logic. En TPHOLs 2007: 20th International Conference on Theorem Proving in Higher Order Logics (135-150), Kaiserslautern, Germany: Springer.
Size: 545.4Kb
Format: PDF

URI: https://hdl.handle.net/11441/74671

DOI: 10.1007/978-3-540-74591-4_11

See editor´s version

This work is under a Creative Commons License: 
Atribución-NoComercial-SinDerivadas 3.0 Estados Unidos de América

This item appears in the following Collection(s)