Verification in ACL2 of a Generic Framework to Synthesize SAT–Provers

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

doi:10.1007/3-540-45013-0_15

Ponencia

dc.creator	Martín Mateos, Francisco Jesús	es
dc.creator	Alonso Jiménez, José Antonio	es
dc.creator	Hidalgo Doblado, María José	es
dc.creator	Ruiz Reina, José Luis	es
dc.date.accessioned	2019-05-16T09:30:02Z
dc.date.available	2019-05-16T09:30:02Z
dc.date.issued	2002
dc.identifier.citation	Martín Mateos, F.J., Alonso Jiménez, J.A., Hidalgo Doblado, M.J. y Ruiz Reina, J.L. (2002). Verification in ACL2 of a Generic Framework to Synthesize SAT–Provers. En LOPSTR 2002: 12th International Workshop on on Logic-Based Program Synthesis and Transformation (182-198), Madrid, España: Springer.
dc.identifier.isbn	978-3-540-40438-5	es
dc.identifier.issn	0302-9743	es
dc.identifier.uri	https://hdl.handle.net/11441/86427
dc.description.abstract	We present in this paper an application of the ACL2 system to reason about propositional satisfiability provers. For that purpose, we present a framework where we define a generic transformation based SAT–prover, and we show how this generic framework can be formalized in the ACL2 logic, making a formal proof of its termination, soundness and completeness. This generic framework can be instantiated to obtain a number of verified and executable SAT–provers in ACL2, and this can be done in an automatized way. Three case studies are considered: semantic tableaux, sequent and Davis–Putnam methods.	es
dc.description.sponsorship	Ministerio de Ciencia y Tecnología TIC2000-1368-C03-02	es
dc.format	application/pdf	es
dc.language.iso	eng	es
dc.publisher	Springer	es
dc.relation.ispartof	LOPSTR 2002: 12th International Workshop on on Logic-Based Program Synthesis and Transformation (2002), p 182-198
dc.rights	Attribution-NonCommercial-NoDerivatives 4.0 Internacional	*
dc.rights.uri	http://creativecommons.org/licenses/by-nc-nd/4.0/	*
dc.title	Verification in ACL2 of a Generic Framework to Synthesize SAT–Provers	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	TIC2000-1368-C03-02	es
dc.relation.publisherversion	https://link.springer.com/chapter/10.1007/3-540-45013-0_15	es
dc.identifier.doi	10.1007/3-540-45013-0_15	es
dc.contributor.group	Universidad de Sevilla. TIC137: Lógica, Computación e Ingeniería del Conocimiento	es
idus.format.extent	17	es
dc.publication.initialPage	182	es
dc.publication.endPage	198	es
dc.eventtitle	LOPSTR 2002: 12th International Workshop on on Logic-Based Program Synthesis and Transformation	es
dc.eventinstitution	Madrid, España	es
dc.relation.publicationplace	Berlin	es

Ficheros	Tamaño	Formato	Ver	Descripción
Verification in ACL2 of a Generic ...	204.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: Attribution-NonCommercial-NoDerivatives 4.0 Internacional