6 The Sharing of Structure in Theorem proving Programs

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.