Article
Constructing Formally Verified Reasoners for the ALC Description Logic
Author/s | Hidalgo Doblado, María José
Alonso Jiménez, José Antonio Martín Mateos, Francisco Jesús Ruiz Reina, José Luis |
Department | Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial |
Publication Date | 2008 |
Deposit Date | 2019-05-07 |
Published in |
|
Abstract | 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. |
Project ID. | TIN2004–03884 |
Citation | 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. |
Files | Size | Format | View | Description |
---|---|---|---|---|
Constructing Formally Verified ... | 404.9Kb | [PDF] | View/ | |