Efficient elimination of Skolem functions in first-order logic without equality.
Ján Komara · arXiv (Cornell University) · 2019
We prove that elimination of a single Skolem function in pure logic increases the length of cut-free proofs only linearly. The result is shown for a variant of sequent calculus with Henkin constants instead of free variables.