MPI-INF/SWS Research Reports 1991-2021
1. Author,Editor - 1. by Individual
MPI-I-92-231
Quantifier elimination in second-order predicate logic
Gabbay, Dov M. and Ohlbach, Hans Jürgen
July 1992, 18 pages.
.Status: available - back from printing
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.
-
92-231.pdf
- Attachement: MPI-I-92-231.dvi (88 KBytes); 92-231.pdf (204 KBytes)
URL to this document: https://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},
}