Eliminating definitions and Skolem functions in first-order logic
Jeremy D. Avigad · ACM Transactions on Computational Logic · 2003
From proofs in any classical first-order theory that proves the existence of at least two elements, one can eliminate definitions in polynomial time. From proofs in any classical first-order theory strong enough to code finite functions, including sequential theories, one can also eliminate Skolem functions in polynomial time.