A Formally Verified Prover for the ALC Description Logic

Alonso Jiménez, José Antonio; Borrego Díaz, Joaquín; Hidalgo Doblado, María José; Martín Mateos, Francisco Jesús; Ruiz Reina, José Luis

doi:10.1007/978-3-540-74591-4_11

Ponencia

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

Ficheros	Tamaño	Formato	Ver	Descripción
A Formally Verified.pdf	545.4Kb	[PDF]	Ver/Abrir

Este registro aparece en las siguientes colecciones

Ponencias (Ciencias de la Computación e Inteligencia Artificial)

Mostrar el registro sencillo del ítem

Excepto si se señala otra cosa, la licencia del ítem se describe como: Atribución-NoComercial-SinDerivadas 3.0 Estados Unidos de América