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

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

The complete lattice of terms


e-mail
Dpto. de Ciencias de la Computación e Inteligencia Artificial
Facultad de Informática y Estadística
Universidad de Sevilla

Reasoning about first-order terms using the ACL2 theorem prover
Last revision: January 24, 2000