*
Computational Logic
Group, CCIA, Universidad de Sevilla, Spain *

We present here the formalization and mechanical proofs in the ACL2 theorem prover of some of the main properties of the lattice of first-order terms. You can see also an antecedent of this work, using NQTHM. This is a brief description of the books:

**
Basic theorems about common data structures
**

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

*ad hoc*compilation of lemmas.*Some properties of association lists: association-lists.events*Properties of finite domain functions.

**
The complete lattice of terms
**

*Definitions and basic properties of first order terms: terms.lisp*We define here several basic concepts about terms, lists of terms, substitutions and application of substitutions to terms.

*Definitions and basic properties of system of equations: system-of-equations.lisp*Some of our rule-based algorithms act on system of equations. This book provides definitions and basic properties.

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

*Definition and verification of a concrete (and executable) subsumption algorithm: subsumption-one-definition-and-properties.lisp*As a particular case of the previous abstract subsumption 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 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.*A*__classical definition__of a subsumption algorithm: subsumption-definition-v0.lispThis book is based on an old events file in Nqthm. A clasical recursive definition is used to define a subsumption algorithm. Although it's not used for the rest of books in this page, the proof techniques used are interesting in its own.

*Renamings (definitions and properties):renamings.lisp*The concept of renaming substitution is defined and some properties are proved. Also two kinds of renamings are proved to be renamings: integer renaming and variable renaming. Renamings are important for two reasons: "starndardization apart" and pretty printing of terms.

*Well-foundedness of subsumption between terms: subsumption-well-founded.lisp*An ordinal measure is given to prove that there is no infinite strictly decreasing chain of subsumed terms. These properties are 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 language and our representation of substitutions. The definition is shown to verify the intended properties.

*Definition and verification of a*__non-deterministic rule-based__unification algorithm: unification-definition.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 the lack of solution) is detected. A partially defined selection function is used to formalize non-determinism.

*Definition and verification of a concrete (and executable) unification algorithm: unification-one-definition.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 we can define in the set of terms of B&M logic a complete lattice structure. To force the existence of glb of every pair of terms, we distinguish a term: the-top-term.

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

Facultad de Informática y Estadística

Universidad de Sevilla

Last revision: January 24, 2000