[ US ] [ CCIA ] [ Teaching ] [ SLC ] [e-mail]
Reasoning about first-order terms using the ACL2 theorem prover

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.lisp

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.

• 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.lisp

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.

• 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.lisp

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.

• 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.

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