TY - INPR
A1 - Autexier, Serge
A1 - Mantel, Heiko
T1 - Semantical Investigation of Simultaneous Skolemization for First-Order Sequent Calculus
N2 - Simultaneous quantifier elimination in sequent calculus is an improvement over the well-known skolemization. It allows a lazy handling of instantiations as well as of the order of certain reductions. We prove the soundness of a sequent calculus which incorporates a rule for simultaneous quantifier elimination. The proof is performed by semantical arguments and provides some insights into the dependencies between various formulas in a sequent.
T3 - SEKI Report - 98,5
KW - skolemization
KW - Simultaneous quantifier elimination
KW - sequent calculus
Y1 - 1998
UR - https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/421
UR - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:hbz:386-kluedo-3922
ER -