series: EUR-FEW-CS 96-14
The subsumption theorem for several forms of resolution
The Subsumption Theorem is the following completeness result for resolution: if S is a set of clauses and C is a clause, then S logically implies C iff C is a tautology, or there exists a clause D which subsumes C, and which can be derived from S by some form of resolution. Different versions of this theorem exist, depending on the kind of resolution we use. It provides a more `direct' form of completeness than the better known refutation-completeness, which often makes the Subsumption Theorem better suited for theoretical research. In this paper we investigate for which forms of resolution the theorem holds, and for which it does not. We collect results earlier obtained by others, and contribute some results of our own. The main results of the paper are as follows. For `unconstrained' resolution, the Subsumption Theorem holds, and is equivalent to the refutation-completeness: the one can be proved from the other. The same is true for linear resolution. For input resolution, the theorem is false, even in the special case where S contains only one clause. In case of SLD-resolution for Horn clauses, the Subsumption Theorem again holds, and is equivalent to the refutation-completeness of SLD-resolution.