@inproceedings{GaOh92c, 
author = "Dov M. Gabbay and Hans J{\"u}rgen Ohlbach",
title = "Quantifier elimination in second--order predicate logic",
booktitle = "Principles of Knowledge Representation and Reasoning (KR92)",
year = 1992,
editor = "Bernhard Nebel and Charles Rich and William Swartout",
pages = "425--435",
publisher = "Morgan Kaufmann",
note = "Also published as a Technical Report MPI-I-92-231, Max-Planck-Institut f{\"u}r Informatik, Saarbr{\"u}cken, and in the {\it South African Computer Journal}, 1992",
abstract = {An algorithm is presented which eliminates second-order 
quantifiers over predicate variables in formulae of type
$\exists P_1 ,..., P_n\ F$ where $F$ is an arbitrary formula of 
first--order predicate logic. The resulting formula is equivalent to 
the original formula - if the algorithm terminates. 
The algorithm can for example be applied to do interpolation, to eliminate the second--order quantifiers in circumscription, 
to compute the correlations between structures and power 
structures, to compute semantic properties corresponding to Hilbert 
axioms in non classical logics and to compute model theoretic 
semantics for new logics.},
keywords = {Quantifier Elimination, Resolution},
source = "ftp://pub/guide/staff/ohlbach/publications/conferences/scan.dvi.gz"}