Lists provide the most obvious and natural representation of literals because lists perfectly reflect function nesting structure. A list is also a reasonable representation of a set, in particular of a clause. Lists, however, can consume large amounts of space, and cause frequent garbage collections. We shall present in this paper a representation of clauses and literals which is as natural as lists but far more compact. We achieve this economy by sharing the structure of the parents of a resolvent in our representation of the resolvent. A clause is a set of literals; but throughout this paper we shall speak of the literals of a clause as having an order. That is, we shall speak of the first, second, etc., literal of a clause.

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.