Presentation
Formalizing Rewriting in the ACL2 Theorem Prover
Author/s | 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 |
Publication Date | 2000 |
Deposit Date | 2019-05-13 |
Published in |
|
ISBN/ISSN | 978-3-540-42071-2 0302-9743 |
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 ... 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. |
Project ID. | PB96-0098-C04-04
PB96-1345 |
Citation | 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. |
Files | Size | Format | View | Description |
---|---|---|---|---|
acl2-rewriting.pdf | 187.4Kb | [PDF] | View/ | |