On the Polynomial Transparency of Resolution

Abstract

In this paper a framework is developed for measuring the complexities of deductions in an abstract and computationally perspicuous manner. As a notion of central importance appears the so-called polynomial transparency of a calculus. If a logic calculus possesses this property, then the complexity of any deduction can be correctly measured in terms of its inference steps. The resolution calculus lacks this property. It is proven that the number of inference steps of a resolution proof does not give a representative measure of the actual complexity of the proof, even if only shortest proofs are considered. We use a class of formulae which have proofs with a polynomial number of inference steps, but for which the size of any proof is exponential. The polynomial intransparency of resolution is due to the renaming of derived clauses, which is a fundamental deduction mechanism. This result motivates the development of new data structures for the representation of logical formulae.