Stalmarck's Method versus Resolution: A Comparative Theoretical Study
Jakob Nordström · 2001
This Master’s thesis presents a comparative analysis of St˚almarck’s proof method and resolution from a theoretical perspective. We give (to our knowledge) the first complete explicit formal description of the dilemma proof system underlying St˚almarck’s method. Based on this description we prove a number of simulation and separation results between different subsystems of dilemma (defined by restrictions on possible branching assumptions and rules for merging the results derived in distinct branches). The key result of the thesis is that dilemma depth translates into resolution width. More precisely, a dilemma refutation in depth d and length L of a k-CNF formula F can be transformed to a resolution refutation of F in width O (kd) and length � Lk d � O(1). From this depth-width relation it follows that for k-CNF formulas with k fixed, resolution p-simulates dilemma restricted to minimum-depth proofs. Furthermore, the running time of the minimum-width proof search algorithm