A Theory About First–Order Terms in ACL2

Abstract. We describe the development in ACL2 of a library of results about first-order terms. In particular, we present the formalization of some of the main properties of the complete lattice of first-order terms with respect to the subsumption relation. As a byproduct, verified executable implementations are obtained for some basic operations on firstorder terms, including matching, renaming, unification and anti-unification. This work can be seen as a basis for further studies about the formal properties of automated reasoning and symbolic computation systems. In [9, 11] we described a formal ACL2 theory about equational reasoning and term rewriting systems. In that work we used a library of definitions and theorems formalizing the lattice theoretic properties of the set of first-order terms with respect to the subsumption relation. Nevertheless, the results of this library have not been documented yet, except the verification of a unification algorithm [10] (in fact, a preliminary Nqthm version). We think that these results are interesting for themselves, so our intention is to describe them in this paper. Our purpose when developing these results about first-order terms is twofold. From a theoretical point of view, we proved in ACL2 that the set of first-order terms in a given signature is a wellfounde