All those who have worked on theorem proving problems in nontrivial domains are familiar with the combinatorial explosion of the size of the search space. Indeed the inevitability of this combinatorial explosion is periodically cited by theorists as the reason why automated theorem proving is a doomed area of research. In most significant systems the search space explodes in two different ways which it is important to distinguish:
The basic idea behind the closure approach is that the second problem is far worse that the first, and that if it can be successfully attacked, then the first problem can be dealt with.
We define the closure approach to be the fundamental paradigm in which formulas that are derived from the initial axioms are kept, and thus are available for use in controlling the growth in the size of the search space. This approach has advantages and disadvantages, corresponding to the fact that keeping clauses both creates and solves the problem of redundancy control.
The principal advantage is that once a formula is derived, it is available for use thereafter whenever needed, and need not be derived again when it appears in another subproof. The two most powerful techniques are subsumption and demodulation, each of which have forward and backward variations. The principal disadvantage is that the actual derivation process cannot be made as fast as it can, for example, by the use of Prolog-style compilation techniques. In addition, some overhead is incurred in keeping the newly-derived formulas and indexing them for later use. The rest of this paper is an historical explanation of how the advantages of the closure approach have outweighed the disadvantages. In the process, we will reveal another important advantage: that the closure approach to theorem proving is extraordinarily flexible in that it can accommodate a very wide variety of variations that have been contrived for it over the years.