COMPLEXITY OF RESOLUTION PROOFS AND FUNCTION INTRODUCTION

The length of resolution proofs is investigated, relative to the model-theoretic measure of Herbrand complexity. A concept of resolution deduction (R-deduction) is introduced which is somewhat more general than the classical concepts. It is shown that proof complexity is exponential in terms of Herbrand complexity and that this bound is tight. The concept of R-deduction is extended to FR-deduction, where, besides resolution, a function introduction rule (based on a re-Skolemization technique) is allowed. As an example, consider the clause P(x, y) v Q(x, y): conclude P(x, f(x)) v Q(a, y), where a, f(x) are new function symbols extending Herbrand's universe. (We use the derivability of (for-all x)(there exists y)P(x, y) v (there exists x)(for-all y)Q(x, y) from (for-all x)(for-all y)(P(x, y) v Q(x, y)) and Skolemization). By modification of a construction of Statman it is shown that FR-deductions may be nonelementarily shorter than R-deductions (thus giving a nonelementary speedup with respect to Herbrand complexity and search space). Finally it is proved that FR-deduction has weaker effects only (maximally double exponential speedup) if clausal logic is restricted to Horn logic.