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
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.
Properties of finite domain functions.
The complete lattice of terms
We define here several basic concepts about terms, lists of terms, substitutions and application of substitutions to terms.
Some of our rule-based algorithms act on system of equations. This book provides definitions and basic properties.
Based in a set of rules that are applied non-deterministically to systems of equations, we define an "abstract" subsumption algorithm, a prove its correctness.
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.
This 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.
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.
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.
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.
An "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.
A particular unification algorithm is defined and verified, as a functional instance of the previously given.
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.
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.
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.