Theorem Proving Based on the Extension Rule

Methods based on resolution have been widely used for theorem proving since it was proposed. This paper presents a new method for theorem proving that uses the inverse of resolution and employs the inclusion-exclusion principle to circumvent the problem of space complexity. We prove its soundness and completeness. The concept of complementary factor is introduced to estimate its complexity. We also show that our method outperforms resolution-based methods in some cases. Thus it is potentially a complementary method to resolution-based methods. This revised version was published online in August 2006 with corrections to the Cover Date.