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.
Metadaten| 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 |
|---|
| Tag: | Simultaneous quantifier elimination ; sequent calculus; skolemization |
|---|
| Faculties / Organisational entities: | Fachbereich Informatik |
|---|
| DDC-Cassification: | 004 Datenverarbeitung; Informatik |
|---|
