Journal of Symbolic Logic · 2012 · 25 citations · 7 references
ComputingComputer ScienceMathematicsAlgorithmsCombinatoricsTheory Of ComputationComputational ComplexityProof ComplexityTheorem ProvingLower BoundsLower Bounds For Proof SystemsProof Size Lower Bounds
Abstract We consider the following problem: Given a proof of the Skolemization of a formula F , what is the length of the shortest proof of F ? For the restriction of this question to cut-free proofs we prove corresponding exponential upper and lower bounds.
7
A compact representation of proofs
Dale Miller · Studia Logica · 1987 · 114 citations
ON SKOLEMIZATION AND PROOF COMPLEXITY
Matthias Baaz, Alexander Leitsch · Fundamenta Informaticae · 1994 · 83 citations
Lower bounds on Herbrand’s theorem
Rick Statman · Proceedings of the American Mathematical Society · 1979 · 83 citations · Full text