dc.creator | Hidalgo Doblado, María José | es |
dc.creator | Alonso Jiménez, José Antonio | es |
dc.creator | Martín Mateos, Francisco Jesús | es |
dc.creator | Ruiz Reina, José Luis | es |
dc.date.accessioned | 2019-05-07T09:09:48Z | |
dc.date.available | 2019-05-07T09:09:48Z | |
dc.date.issued | 2008 | |
dc.identifier.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. | |
dc.identifier.issn | 1571-0661 | es |
dc.identifier.uri | https://hdl.handle.net/11441/86251 | |
dc.description.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 (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. | es |
dc.description.sponsorship | Ministerio de Educación y Ciencia TIN2004–03884 | es |
dc.format | application/pdf | es |
dc.language.iso | eng | es |
dc.publisher | Elsevier | es |
dc.relation.ispartof | Electronic Notes in Theoretical Computer Science, 200 (3), 87-102. | |
dc.rights | Attribution-NonCommercial-NoDerivatives 4.0 Internacional | * |
dc.rights.uri | http://creativecommons.org/licenses/by-nc-nd/4.0/ | * |
dc.subject | Semantic Web | es |
dc.subject | Description Logics | es |
dc.subject | Verification | es |
dc.subject | Formal Methods | es |
dc.title | Constructing Formally Verified Reasoners for the ALC Description Logic | es |
dc.type | info:eu-repo/semantics/article | es |
dcterms.identifier | https://ror.org/03yxnpp24 | |
dc.type.version | info:eu-repo/semantics/submittedVersion | es |
dc.rights.accessRights | info:eu-repo/semantics/openAccess | es |
dc.contributor.affiliation | Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial | es |
dc.relation.projectID | TIN2004–03884 | es |
dc.relation.publisherversion | https://www.sciencedirect.com/science/article/pii/S1571066108003095 | es |
dc.identifier.doi | 10.1016/j.entcs.2008.04.094 | es |
dc.contributor.group | Universidad de Sevilla. TIC137: Lógica, Computación e Ingeniería del Conocimiento | es |
idus.format.extent | 16 | es |
dc.journaltitle | Electronic Notes in Theoretical Computer Science | es |
dc.publication.volumen | 200 | es |
dc.publication.issue | 3 | es |
dc.publication.initialPage | 87 | es |
dc.publication.endPage | 102 | es |
dc.identifier.sisius | 6606456 | es |