A comparative study of several proof procedures

摘要

In this paper three algorithms for testing the complementarity of a matrix (representing a propositional formula) are developed in stages. Any of these algorithms is distinguished from its predecessor by a specific feature (linearity, jump, non-normal form) which endows it with a provable advantage w.r.t. its performance. For well-known proof procedures it is shown that they can be simulated by at least one of these algorithms which provides a hierarchy among several ATP-methods.