dc.creator | Ruiz Reina, José Luis | es |
dc.creator | Alonso Jiménez, José Antonio | es |
dc.creator | Hidalgo Doblado, María José | es |
dc.creator | Martín Mateos, Francisco Jesús | es |
dc.date.accessioned | 2019-05-09T08:46:52Z | |
dc.date.available | 2019-05-09T08:46:52Z | |
dc.date.issued | 2002 | |
dc.identifier.citation | Ruiz Reina, J.L., Alonso Jiménez, J.A., Hidalgo Doblado, M.J. y Martín Mateos, F.J. (2002). Formal proofs about rewriting using ACL2. Annals of Mathematics and Artificial Intelligence, 36 (3), 239-262. | |
dc.identifier.issn | 1012-2443 | es |
dc.identifier.uri | https://hdl.handle.net/11441/86266 | |
dc.description.abstract | We present an application of the ACL2 theorem prover to reason about rewrite systems
theory. We describe the formalization and representation aspects of our work using the firstorder,
quantifier-free logic of ACL2 and we sketch some of the main points of the proof effort.
First, we present a formalization of abstract reduction systems and then we show how this
abstraction can be instantiated to establish results about term rewriting. The main theorems
we mechanically proved are Newman’s lemma (for abstract reductions) and Knuth–Bendix
critical pair theorem (for term rewriting). | es |
dc.description.sponsorship | Ministerio de Educación y Ciencia TIC2000-1368-CO3-02 | es |
dc.format | application/pdf | es |
dc.language.iso | eng | es |
dc.publisher | Springer | es |
dc.relation.ispartof | Annals of Mathematics and Artificial Intelligence, 36 (3), 239-262. | |
dc.rights | Attribution-NonCommercial-NoDerivatives 4.0 Internacional | * |
dc.rights.uri | http://creativecommons.org/licenses/by-nc-nd/4.0/ | * |
dc.subject | Theorem proving | es |
dc.subject | ACL2 | es |
dc.subject | Rewriting | es |
dc.subject | Formal verification | es |
dc.title | Formal proofs about rewriting using ACL2 | 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-CO3-02 | es |
dc.relation.publisherversion | https://link.springer.com/article/10.1023/A:1016003314081 | es |
dc.identifier.doi | 10.1023/A:1016003314081 | es |
dc.contributor.group | Universidad de Sevilla. TIC137: Lógica, Computación e Ingeniería del Conocimiento | es |
idus.format.extent | 24 | es |
dc.journaltitle | Annals of Mathematics and Artificial Intelligence | es |
dc.publication.volumen | 36 | es |
dc.publication.issue | 3 | es |
dc.publication.initialPage | 239 | es |
dc.publication.endPage | 262 | es |
dc.identifier.sisius | 6629808 | es |