dc.creator | Alonso Jiménez, José Antonio | es |
dc.creator | Borrego Díaz, Joaquín | es |
dc.creator | Hidalgo Doblado, María José | es |
dc.creator | Martín Mateos, Francisco Jesús | es |
dc.creator | Ruiz Reina, José Luis | es |
dc.date.accessioned | 2018-05-16T08:32:13Z | |
dc.date.available | 2018-05-16T08:32:13Z | |
dc.date.issued | 2007 | |
dc.identifier.citation | 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. | |
dc.identifier.isbn | 978-3-540-74590-7 | es |
dc.identifier.issn | 0302-9743 | es |
dc.identifier.uri | https://hdl.handle.net/11441/74671 | |
dc.description.abstract | 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. | 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 | Springer | es |
dc.relation.ispartof | TPHOLs 2007: 20th International Conference on Theorem Proving in Higher Order Logics (2007), p 135-150 | |
dc.rights | Atribución-NoComercial-SinDerivadas 3.0 Estados Unidos de América | * |
dc.rights.uri | http://creativecommons.org/licenses/by-nc-nd/4.0/ | * |
dc.title | A Formally Verified Prover for the ALC Description Logic | es |
dc.type | info:eu-repo/semantics/conferenceObject | 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://link.springer.com/chapter/10.1007/978-3-540-74591-4_11 | es |
dc.identifier.doi | 10.1007/978-3-540-74591-4_11 | es |
idus.format.extent | 16 | es |
dc.publication.initialPage | 135 | es |
dc.publication.endPage | 150 | es |
dc.eventtitle | TPHOLs 2007: 20th International Conference on Theorem Proving in Higher Order Logics | es |
dc.eventinstitution | Kaiserslautern, Germany | es |
dc.relation.publicationplace | Berlín | es |
dc.identifier.sisius | 6527573 | es |
dc.contributor.funder | Ministerio de Educación y Ciencia (MEC). España | |