Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society


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.
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.pdf92-231.pdfMPI-I-92-231.dvi88 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:
Hide details for BibTeXBibTeX
  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},