Repositorio de producción científica de la Universidad de Sevilla

Formal proofs about rewriting using ACL2

 

Advanced Search
 
Opened Access Formal proofs about rewriting using ACL2
Cites

Show item statistics
Icon
Export to
Author: Ruiz Reina, José Luis
Alonso Jiménez, José Antonio
Hidalgo Doblado, María José
Martín Mateos, Francisco Jesús
Department: Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial
Date: 2002
Published in: Annals of Mathematics and Artificial Intelligence, 36 (3), 239-262.
Document type: Article
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).
Cite: 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.
Size: 253.8Kb
Format: PDF

URI: https://hdl.handle.net/11441/86266

DOI: 10.1023/A:1016003314081

See editor´s version

This work is under a Creative Commons License: 
Attribution-NonCommercial-NoDerivatives 4.0 Internacional

This item appears in the following Collection(s)