Complexity of resolution proofs and function introduction (Q1194246)

The function introduction rule derives from the clause \(C=F_ 1\lor F_ 2\) (with free variables \(y_ 1,\dots,y_ k)\) the Skolemised form of the formula \(C'=Q_ 1 y_ 1 Q_ 2 y_ 2\cdots Q_ k y_ k F_ 1\lor Q_ 1' y_ 1 Q_ 2' y_ 2\cdots Q_ k' y_ k\), where \(Q_ i\) are quantifiers, \(\forall'=\exists\), \(\exists'=\forall\). Since \(C\to C'\) is valid, this rule preserves unsatisfiability. Using Statman's sequence of formulas exhibiting non-elementary speed-up over Herbrand expansions, the authors obtain non-elementary speed-up over resolution for one application of the function introduction rule.