arXiv Analytics

Sign in

arXiv:1909.01697 [math.LO]AbstractReferencesReviewsResources

Efficient elimination of Skolem functions in first-order logic without equality

Ján Komara

Published 2019-09-04Version 1

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.

Comments: 20 pages
Categories: math.LO, cs.LO
Subjects: 03F03, 03F20, F.4.1
Related articles: Most relevant | Search more
arXiv:2207.07397 [math.LO] (Published 2022-07-15)
First-order logic with self-reference
arXiv:2208.11354 [math.LO] (Published 2022-08-24)
Non-distributive positive logic as a fragment of first-order logic over semilattices
arXiv:1404.4004 [math.LO] (Published 2014-04-15)
One-dimensional fragment of first-order logic

Links

Toolbox