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

A Formally Verified Prover for the ALC Description Logic

Opened Access A Formally Verified Prover for the ALC Description Logic

Citas

buscar en

Estadísticas
Icon
Exportar a
Autor: 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
Departamento: Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial
Fecha: 2007
Publicado en: 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
Tipo de documento: Ponencia
Resumen: 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.
Cita: 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.
Tamaño: 545.4Kb
Formato: PDF

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

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

Ver versión del editor

Mostrar el registro completo del ítem


Esta obra está bajo una Licencia Creative Commons Atribución-NoComercial-SinDerivadas 3.0 Estados Unidos de América

Este registro aparece en las siguientes colecciones