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

Formalizing Rewriting in the ACL2 Theorem Prover

 

Advanced Search
 
Opened Access Formalizing Rewriting in the ACL2 Theorem Prover
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: 2000
Published in: AISC 2000: International Conference on Artificial Intelligence and Symbolic Computation (2000), p 92-106
ISBN/ISSN: 978-3-540-42071-2
0302-9743
Document type: Presentation
Abstract: We present an application of the ACL2 theorem prover to formalize and reason about rewrite systems theory. This can be seen as a first approach to apply formal methods, using ACL2, to the design of symbolic computation systems, since the notion of rewriting or simplification is ubiquitous in such systems. We concentrate here on formalization and representation aspects of abstract reduction and term rewriting systems, using the first-order, quantifier-free ACL2 logic based on Common Lisp.
Cite: Ruiz Reina, J.L., Alonso Jiménez, J.A., Hidalgo Doblado, M.J. y Martín Mateos, F.J. (2000). Formalizing Rewriting in the ACL2 Theorem Prover. En AISC 2000: International Conference on Artificial Intelligence and Symbolic Computation (92-106), Madrid, España: Springer.
Size: 187.4Kb
Format: PDF

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

DOI: 10.1007/3-540-44990-6_7

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)