DocumentCode :
3223253
Title :
Eliminating definitions and Skolem functions in first-order logic
Author :
Avigad, Jeremy
Author_Institution :
Dept. of Philos., Carnegie Mellon Univ., Pittsburgh, PA, USA
fYear :
2001
fDate :
2001
Firstpage :
139
Lastpage :
146
Abstract :
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. The author considers how 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
Keywords :
formal logic; theorem proving; Skolem functions; classical first-order theory; finite functions; first-order logic; polynomial bound; proof length; sequential theories; Arithmetic; Computer science; Constraint theory; Logic; Polynomials; Upper bound;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Logic in Computer Science, 2001. Proceedings. 16th Annual IEEE Symposium on
Conference_Location :
Boston, MA
ISSN :
1043-6871
Print_ISBN :
0-7695-1281-X
Type :
conf
DOI :
10.1109/LICS.2001.932490
Filename :
932490
Link To Document :
بازگشت