[ US ] [ CCIA ] [ Teaching ] [ SLC ] [e-mail]
Formalizing equational reasoning and rewriting (using ACL2)

Computational Logic Group, CCIA, University of Seville, Spain

UPDATED: July 17th, 2001.

We present here a formalization and mechanical proofs in the ACL2 system of some of the main properties of equational reasoning, mainly rewriting. You can see also an antecedent of this work, using NQTHM. The following is a exhaustive list of the books we have developed so far, with a brief description.

Multisets relations

Abstract relations and abstract proofs

The complete lattice of terms

Equational theories and rewriting

Decidability of equational theories given by complete term rewriting systems

All the books are tared and gziped in acl2-equational.tgz.

To certify the books, see the README file.

Some related papers

  • Mechanical verification of a rule based unification algorithm in the Boyer-Moore theorem prover, presented at AGP'99. And also the slides.
  • Multiset relations: a tool for proving termination, presented at ACL2 Workshop 2000. Here are the slides.
  • A Theory About First-order Terms in ACL2, presented at ACL2 Workshop 2002, with the slides.
  • Formalizing rewriting in the ACL2 theorem prover Springer-Verlag ), presented at AISC 2000, and the slides
  • A mechanical proof of Knuth-Bendix critical pair theorem (using ACL2), presented at FTP 2000. Here are the slides.

    Dpto. de Ciencias de la Computación e Inteligencia Artificial
    Universidad de Sevilla

    Formalizing equational reasoning and rewriting (using ACL2)