Simultaneous Quantifier Elimination

摘要

We present a sequent calculus which allows the simultaneous elimination of multiple quantifiers. The approach is an improvement over the well-known skolemization in sequent calculus. It allows a lazy handling of instantiations and of the order of certain reductions. Simultaneous quantifier elimination is justified from a semantical as well as from a proof theoretical point of view.