Hidalgo Doblado, María JoséAlonso Jiménez, José AntonioMartín Mateos, Francisco JesúsRuiz Reina, José Luis2019-05-072019-05-072008Hidalgo 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.1571-0661https://hdl.handle.net/11441/86251Description 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.application/pdfengAttribution-NonCommercial-NoDerivatives 4.0 Internacionalhttp://creativecommons.org/licenses/by-nc-nd/4.0/Semantic WebDescription LogicsVerificationFormal Methodsinfo:eu-repo/semantics/articleinfo:eu-repo/semantics/openAccesshttps://doi.org/10.1016/j.entcs.2008.04.094