Resolution Plans in Theorem Proving

Abstract

Briefly, an example of a resolution plan can be described as follows: Let Ll v A and L2 v B be two clauses, where Ll and L2 are literals, and A and B are clauses. If Ll and L2 can be made complementary by some substitution, we shall call A v B (Ll,L2) a resolution plan. In general, a resolution plan is represented by C (Ll,Ml) ••. (Lr,Mr) , where Ll,Ml, ... ,Lr,Mr are literals, and Cis a clause. If Cis empty, (Ll,Ml) .•• (Lr,Mr) is called a total plan. The total plan corresponds to a proof if there is a unifier which simultaneously make (Li,Mi) complementary, i•l, ••. ,r. As shown elsewhere, the total plan approach can eliminate redundancies. In this paper, we shall show that all the strategies developed for resolution can be used to generate total plans.