Artículo
Constructing Formally Verified Reasoners for the ALC Description Logic
Autor/es | Hidalgo Doblado, María José
Alonso Jiménez, José Antonio 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 de publicación | 2008 |
Fecha de depósito | 2019-05-07 |
Publicado en |
|
Resumen | Description Logics are a family of logics used to represent and reason about conceptual and terminological
knowledge. Recently, its importance has been increased since they are used as a basis for the Ontology
Web Language ... Description Logics are a family of logics used to represent and reason about conceptual and terminological knowledge. Recently, its importance has been increased since they are used as a basis for the Ontology Web Language (OWL) used for the Semantic Web. In previous work, we have developed in PVS a generic framework for reasoning in the ALC description logic, proving its termination, soundness and completeness. In this paper we present the construction, from the generic framework, of a formally verified generic tableau– based algorithm for checking satisfiability of ALC –concepts. We do it using a methodology of refinements to transfer the properties from the framework to the algorithm. We also obtain some verified reasoners from the algorithm by a process of instantiation. |
Identificador del proyecto | TIN2004–03884 |
Cita | Hidalgo Doblado, M.J., Alonso Jiménez, J.A., Martín Mateos, F.J. y Ruiz Reina, J.L. (2008). Constructing Formally Verified Reasoners for the ALC Description Logic. Electronic Notes in Theoretical Computer Science, 200 (3), 87-102. |
Ficheros | Tamaño | Formato | Ver | Descripción |
---|---|---|---|---|
Constructing Formally Verified ... | 404.9Kb | [PDF] | Ver/ | |