Paper: Eliminating Definitions and Skolem Functions in First-Order Logic (at LICS 2001)
Authors: Jeremy AvigadAbstract
In any classical first-order theory that proves the existence of at least two elements, one can eliminate definitions with a polynomial bound on the increase in proof length. In any classical first-order theory strong enough to code finite functions, including sequential theories, one can also eliminate Skolem functions with a polynomial bound on the increase in proof length.
BibTeX
@InProceedings{Avigad-EliminatingDefiniti, author = {Jeremy Avigad}, title = {Eliminating Definitions and Skolem Functions in First-Order Logic}, booktitle = {Proceedings of the Sixteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2001}, year = 2001, editor = {Joseph Halpern}, month = {June}, pages = {139--146}, location = {Boston, MA, USA}, publisher = {IEEE Computer Society Press} }