Artículo
Formal proofs about rewriting using ACL2
Autor/es | Ruiz Reina, José Luis
Alonso Jiménez, José Antonio Hidalgo Doblado, María José Martín Mateos, Francisco Jesús |
Departamento | Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial |
Fecha de publicación | 2002 |
Fecha de depósito | 2019-05-09 |
Publicado en |
|
Resumen | 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 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). |
Identificador del proyecto | TIC2000-1368-CO3-02 |
Cita | 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. |
Ficheros | Tamaño | Formato | Ver | Descripción |
---|---|---|---|---|
Formal Proofs About Rewriting ... | 253.8Kb | [PDF] | Ver/ | |