SCAN—Elimination of predicate quantifiers

Abstract

Some higher-order formulas are equivalent to formulas of first-order predicate logic or even propositional logic. In applications where formulas of higherorder predicate logic occur naturally it is very useful to determine whether the given formula is in fact equivalent to a simpler formula of first-order or prepositional logic. Typical applications where this occurs are predicate minimization by circumscription, correspondence theory in non-classical logics and simple versions of set theory. In these areas we are faced with formulas of second-order predicate logic with existentially or universally quantified predicate variables and want to simplify them by computing equivalent first-order formulas.

In general this problem is not even semi-decidable, so no complete quantifier elimination algorithms for predicate quantifiers can exist. Nevertheless, some of the proposed algorithms are quite powerful and can solve hard problems in the areas mentioned above.

In this paper the implementation of the scan algorithm¹ proposed by Gabbay and Ohlbach [GO92b] is described. Besides the basic quantifier elimination algorithm, interfaces for computing first-order circumscription and correspondence axioms in non-classical logics are available. The interfaces translate the given problem specification into a quantifier elimination problem and invoke the basic algorithm.