Simultaneous quantifier elimination

Publikationstyp
Conference Paper
Publikationsdatum
1998-09
Sprache
English
Author
Autexier, Serge 
Mantel, Heiko 
Stephan, Werner 
TORE-URI
http://hdl.handle.net/11420/14037
First published in
Lecture notes in computer science 
Number in series
1504 LNA
Start Page
141
End Page
152
Citation
Lecture Notes in Computer Science 1504 LNA: 141-152 (1998)
Contribution to Conference
22nd Annual German Conference on Artificial Intelligence, KI 1998 
Publisher DOI
10.1007/BFb0095435
Scopus ID
2-s2.0-84957094660
Publisher
Springer
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.
DDC Class
004: Informatik