Show simple item record

dc.creatorMartín Mateos, Francisco Jesúses
dc.creatorAlonso Jiménez, José Antonioes
dc.creatorHidalgo Doblado, María Josées
dc.creatorRuiz Reina, José Luises
dc.date.accessioned2019-05-16T09:30:02Z
dc.date.available2019-05-16T09:30:02Z
dc.date.issued2002
dc.identifier.citationMartí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.isbn978-3-540-40438-5es
dc.identifier.issn0302-9743es
dc.identifier.urihttps://hdl.handle.net/11441/86427
dc.description.abstractWe 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.sponsorshipMinisterio de Ciencia y Tecnología TIC2000-1368-C03-02es
dc.formatapplication/pdfes
dc.language.isoenges
dc.publisherSpringeres
dc.relation.ispartofLOPSTR 2002: 12th International Workshop on on Logic-Based Program Synthesis and Transformation (2002), p 182-198
dc.rightsAttribution-NonCommercial-NoDerivatives 4.0 Internacional*
dc.rights.urihttp://creativecommons.org/licenses/by-nc-nd/4.0/*
dc.titleVerification in ACL2 of a Generic Framework to Synthesize SAT–Proverses
dc.typeinfo:eu-repo/semantics/conferenceObjectes
dc.type.versioninfo:eu-repo/semantics/submittedVersiones
dc.rights.accessrightsinfo:eu-repo/semantics/openAccesses
dc.contributor.affiliationUniversidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificiales
dc.relation.projectIDTIC2000-1368-C03-02es
dc.relation.publisherversionhttps://link.springer.com/chapter/10.1007/3-540-45013-0_15es
dc.identifier.doi10.1007/3-540-45013-0_15es
dc.contributor.groupUniversidad de Sevilla. TIC137: Lógica, Computación e Ingeniería del Conocimientoes
idus.format.extent17es
dc.publication.initialPage182es
dc.publication.endPage198es
dc.eventtitleLOPSTR 2002: 12th International Workshop on on Logic-Based Program Synthesis and Transformationes
dc.eventinstitutionMadrid, Españaes
dc.relation.publicationplaceBerlines

FilesSizeFormatViewDescription
Verification in ACL2 of a Generic ...204.4KbIcon   [PDF] View/Open  

This item appears in the following collection(s)

Show simple item record

Attribution-NonCommercial-NoDerivatives 4.0 Internacional
Except where otherwise noted, this item's license is described as: Attribution-NonCommercial-NoDerivatives 4.0 Internacional