A Sequential Theorem Proving Algorithm without Deletion

We present here a simplified form of the theorem-proving algorithm that has been used in Argonne systems over the years [9,4,5]. For an introduction to the approach, see [10]. We assume that the goal is to prove a set of clauses unsatisfiable. We assume further that the input clauses are divided into two sets, which we call the ``axioms'' and the ``set of support'', in such a way that the axioms are satisfiable. (If the input clauses make this difficult to do, then the axioms may be chosen to be the empty set.) Thus we will be using the ``set-of-support strategy'' first described in [8].

  

Figure: Sequential Theorem-Proving Algorithm without Deletion (Algorithm 1)

1#1

The algorithm given in Figure can complete with the empty clause found (giving a proof that the input clause set is unsatisfiable), compete without the empty clause being found (no proof), or it can fail to terminate with the constraints of time and memory. If the filtering mechanism applied is appropriately chosen, then this scheme is complete: that is, if the algorithm terminates without finding the empty clause, then the original set of clauses is satisfiable.

The currently most effective implementation of this algorithm is OTTER[5]. OTTER has a wide variety of inference rules and control parameters for adapting this algorithm to a particular problem and sophisticated indexing methods to make each of the operations quite fast, even when the set of kept clauses has grown to hundred thousand clauses or more.

This particular approach contrasts with some more recent ``Prolog technology'' theorem provers[6] [PTTP,Plaisted?], which use the compilation techniques from WAM-based Prolog implementations to achieve extremely high inference rates, at a cost of possibly redundant computations. The ``closure'' approach taken here is based on the expectation that a clause deduced and processed is worth keeping as a filter for preventing the deduction and subsequent use of duplicate or weaker clauses. Experience is on the side of the closure approach; although certain small problems can be done very quickly with the Prolog-technology approach, many large problems done years ago with the closure approach remain out of reach of even the best Prolog technology systems. Some examples are given in Sections and below.