On the complexity of proof deskolemization
Matthias Baaz, Stefan Hetzl, Daniel S. Weller · Journal of Symbolic Logic · 2012
Abstract We consider the following problem: Given a proof of the Skolemization of a formulaF, what is the length of the shortest proof ofF? For the restriction of this question to cut-free proofs we prove corresponding exponential upper and lower bounds.