*
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
**

*Multisets orderings: multiset.lisp*This book formalizes (in ACL2) Dershowitz and Manna's theorem about multiset orderings: every well-founded relation on a set can be "extended" to a well-founded relation on multisets (lists) of elements of the set. This kind of orderings is very useful in proving properties of equational reasoning.

*The defmul macro: defmul.lisp*This book includes

*multiset.lisp*and defines a macro named*defmul*to build (well-founded) multiset extensions induced by (well-founded) ACL2 relations.*Case studies of using defmul: mccarthy-91.lisp and ackermann.lisp*.Two examples given by Dershowitz and Manna, formalized in ACL2. We use

*defmul*to prove termination of an iterative version of McCarthy's 91 function and termination of a tail-recursive version of Ackermann's function. But the main application of*defmul*is a__mechanical proof of Newman's lemma__, as shown below.

**
Abstract relations and abstract proofs
**

*Abstract proofs: abstract-proofs.lisp*We see here proofs from a very general point of view. Proofs are chains of r-steps, and r-steps are structures with four fields:

*elt1*,*elt2*,*direct*and*operator*(every step "connect"*elt1*and*elt2*in the orientation given by*direct*,and by application of*operator*). Nothing more is assumed about an "abstract proof".*Confuence and proofs: confluence.lisp*We define in this book the concept of confluent (Church-Rosser) and normalizing reduction relation, and prove that the reflexive-symmetric-transitive closure of a confluent and normalizing reduction relation is decidable (provided normal forms are computable). We treat proofs as manipulable objects, and we define some "operations" acting on proofs (an

*algebra*of proofs).*Newman's lemma: newman.lisp*We formalize in this book locally confluent and noetherian reduction relations, and prove Newman's lemma: local confluence of noetherian relations implies Church-Rosser property.

*Convergence: convergent.lisp*Using the results of

*confluence.lisp*and*newman.lisp*and the`encapsulate/functional-instanciation`mechanism, we show decidability of the equivalence closure of every noetherian and locally confluent reduction relation.*A case study, instantiating the abstract framework: perm.lisp*This is a naive example of how to instantiate the abstract framework in order to prove properties of a concrete reduction relation, whose equivalence closure is the "permutation of lists" relation. But the main instantiation of this abstract framework is the "term rewriting" reduction, as shown below.

**
The complete lattice of terms
**

*Some properties and previous basic results: basic.lisp*This book contains lemmas about lists, finite multisets, finite sets, and association lists needed for our proofs. This file is not intended to be a good formalization for that theory, but and

*ad hoc*compilation of lemmas.*Definitions and basic properties of first order terms: terms.lisp*We define here several basic concepts about terms, lists of terms, substitutions and equations.

*Definition and verification of*__rule-based__matching algorithm: matching.lispBased in a set of rules that are applied non-deterministically to systems of equations, we define an "abstract" matching algorithm, a prove its correctness.

*Definition and verification of a concrete (and executable) subsumption algorithm: subsumption.lisp*As a particular case of the previous abstract matching algorithm, we define a concrete subsumption algorithm. This algorithm, given two terms, returns, whenever it exists, a substitution such that applied to the first term gives the second. Its verification is done using functional instantiation. Also it is shown that subsumption is a quasi-ordering and several additional properties. These properties are proved using

__only__the soundness and completeness theorem of the defined algorithm.*Renamings (definitions and properties): renamings.lisp*The concept of renaming substitution is defined and some properties are proved. Also, equivalence of terms (w.r.t subsumption) is defined. Finally, a particular kind of renaming is proved to be a renaming: number renaming. Renamings are important for some reasons: "standardization apart" and pretty printing of terms, for example.

*Well-foundedness of subsumption between terms: subsumption-well-founded.lisp*An ordinal measure is given to justify that there is no infinite strictly decreasing chain of subsumed terms. That property is proved using

__only__the soundness and completeness theorem of the defined subsumption algorithm.*Definition and properties of subsumption between substitutions: subsumption-subst.lisp*A suitable definition of subsumption between substitutions is given, avoiding some restrictions imposed by the ACL2 logic and our representation of substitutions. The definition is shown to verify the intended properties.

*Definition and verification of a*__rule-based__unification algorithm: unification-pattern.lispAn "abstract" unification algorithm is defined and verified. This unification algorithm is defined as a set of transformations rules acting on sets of equations, based on the ones given by Martelli and Montanari. These rules are non-deterministically applied until a solution (or unsolvability) is detected. A partially defined selection function is used to formalize non-determinism.

*Definition and verification of a concrete (and executable) unification algorithm: unification.lisp*A particular unification algorithm is defined and verified, as a functional instance of the previously given.

*Definition and verification of an anti-unification algorithm: anti-unification.lisp*An anti-unification algorithm is defined and verified. This anti-unification algorithm, given two terms, returns a common generalization, subsumed by any other common generalization. Thus, we proved the existence of a least upper bound of two given terms, with respect to subsumption.

*Definition and verification of a most general instance algorithm: mg-instance.lisp*An "most general instance" algorithm is defined and verified. This algorithm, given two terms, returns a common instance, that subsumes any other common instance. Thus, we proved the existence of a greatest lower bound of two given terms, with respect to subsumption.

*The complete lattice of terms: lattice-of-terms.lisp*Just for mathematical recreation (and as a compilation of the previous books) we proved that the set of first-order term in a signature (with an additional top term) is a well-founded lattice.

**
Equational theories and rewriting
**

*Definition of the equational theory given by a set of equational axioms: equational-theories.lisp*We define here several concepts about equational deduction: equational operators and equational proofs. We also extend the algebra of proofs with the operations of instantiation and context. Using this approach, we prove that equational equivalence is the least equivalence relation defined in the set of terms, in a given signature, closed under instantiation and inclusion in contexts, and containing the equational axioms.

*Definitions and basic properties of rewrite systems: rewriting.lisp*Equations can be seen as reduction rules in rewrite systems. The concept of reducibility is defined and a reducibility algorithm is proved to implement the concept. Noetherian rewrite systems are also defined by means of reduction orderings, and in this case the reduced terms are proved to decrease with respect to a well founded relation. Finally, a naive algorithm to compute a normal form w.r.t. a noetherian term rewriting system is defined and verified.

**
Decidability of equational theories given by complete term
rewriting systems
**

*Critical pair lemma: critical-pairs.lisp*The concept of critical pair between two rules is defined and Knuth-Bendix critical pair lemma is proved: A rewrite system is locally confluent if all its critical pairs are joinable. Additionally, we define and verify a function to compute all the critical pairs of a term rewriting system.

*Decidability of confluent and terminating rewrite systems: kb-decidability.lisp*Using the books

*critical-pairs.lisp*and*convergent.lisp*, we prove that if all the critical pairs of a noetherian term rewriting system*R*have common normal forms, then the equational theory described by*R*is decidable.

To certify the books, see the README file.

*Some related papers*

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

Universidad de Sevilla