hide
Free keywords:
-
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.
