The sharing of structure in theorem-proving programs

We describe how clauses in resolution programs can be represented and used Without applying substitutions or cons-ing lists of literals. The amount of space required by our representation of a clause is independent of the number of literals in the clause and the depth of function nesting. We introduce the concept of the value of an expression in a binding environment which we use to standardize clauses apart and share the structure of parents in representing the resolvent.