# Item

ITEM ACTIONSEXPORT

Released

Report

#### Quantifier Elimination in Second-order Predicate Logic

##### Fulltext (public)

MPI-I-92-231.pdf

(Any fulltext), 27MB

##### Supplementary Material (public)

There is no public supplementary material available

##### Citation

Gabbay, D. M., & Ohlbach, H. J.(1992). *Quantifier Elimination
in Second-order Predicate Logic* (MPI-I-92-231). Saarbrücken: Max-Planck-Institut für Informatik.

Cite as: http://hdl.handle.net/11858/00-001M-0000-0014-B72E-6

##### Abstract

An algorithm is presented which eliminates second-order
quantifiers over predicate variables in formulae of type
exists P1 ,..., Pn 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.