Semantical Investigation of Simultaneous Skolemization for First-Order Sequent Calculus
- 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.
Download full text files
Export metadata
Additional Services
| Author: | Serge Autexier, Heiko Mantel |
|---|---|
| URN (permanent link): | urn:nbn:de:hbz:386-kluedo-3922 |
| Serie (Series number): | SEKI Report (98,5) |
| Document Type: | Preprint |
| Language of publication: | English |
| Year of Completion: | 1998 |
| Year of Publication: | 1998 |
| Publishing Institute: | Technische Universität Kaiserslautern |
| Date of the Publication (Server): | 2000/04/03 |
| Tag: | Simultaneous quantifier elimination ; sequent calculus; skolemization |
| Faculties / Organisational entities: | Fachbereich Informatik |
| DDC-Cassification: | 0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik |
| Licence (German): | Standard gemäß KLUEDO-Leitlinien vor dem 27.05.2011 |
