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-10T09:26:50Z | |
dc.date.available | 2019-05-10T09:26:50Z | |
dc.date.issued | 2004 | |
dc.identifier.citation | Martín Mateos, F.J., Alonso Jiménez, J.A., Hidalgo Doblado, M.J. y Ruiz Reina, J.L. (2004). Formal verification of a generic framework to synthesize SAT-provers. Journal of Automated Reasoning, 32 (287) | |
dc.identifier.issn | 0168-7433 | es |
dc.identifier.uri | https://hdl.handle.net/11441/86269 | |
dc.description.abstract | We present in this paper an application of the ACL2 system to generate
and reason about propositional satis ability provers. For that purpose, we develop a
framework where we de ne a generic SAT-prover based on transformation rules, and
we formalize this generic framework in the ACL2 logic, carrying out a formal proof of
its termination, soundness and completeness. This generic framework can be
instantiated to obtain a number of veri ed and executable SAT-provers in ACL2, and
this can be done in an automated way. Three instantiations of the generic framework
are considered: semantic tableaux, sequent and Davis-Putnam-Logeman-Loveland
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 | Journal of Automated Reasoning, 32 (287) | |
dc.rights | Attribution-NonCommercial-NoDerivatives 4.0 Internacional | * |
dc.rights.uri | http://creativecommons.org/licenses/by-nc-nd/4.0/ | * |
dc.title | Formal verification of a generic framework to synthesize SAT-provers | 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 | TIC2000-1368-C03-02 | es |
dc.relation.publisherversion | https://link.springer.com/article/10.1007/BF03177742 | es |
dc.identifier.doi | 10.1007/BF03177742 | es |
dc.contributor.group | Universidad de Sevilla. TIC137: Lógica, Computación e Ingeniería del Conocimiento | es |
idus.format.extent | 30 | es |
dc.journaltitle | Journal of Automated Reasoning | es |
dc.publication.volumen | 32 | es |
dc.publication.issue | 287 | es |