# MPI-I-92-231

## Quantifier elimination in second-order predicate logic

### Gabbay, Dov M. and Ohlbach, Hans Jürgen

**MPI-I-92-231**. July** **1992, 18 pages. | Status:** **available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:

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.

Acknowledgement:** **

References to related material:

To download this research report, please select the type of document that fits best your needs. | Attachement Size(s): |

92-231.pdf | 88 KBytes; 204 KBytes |

Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView |

**URL to this document: **http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1992-231

**BibTeX**
`@TECHREPORT{``GabbayOhlbach92``,`

` AUTHOR = {Gabbay, Dov M. and Ohlbach, Hans J{\"u}rgen},`

` TITLE = {Quantifier elimination in second-order predicate logic},`

` TYPE = {Research Report},`

` INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},`

` ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},`

` NUMBER = {MPI-I-92-231},`

` MONTH = {July},`

` YEAR = {1992},`

` ISSN = {0946-011X},`

`}`