SCAN

The Theory

The Basic Idea
References

The Basic Idea

SCAN is an algorithm that takes as input a second-order predicate logic formula exists P1...Pn phi(Pi) with existentially quantified predicate variables Pi and a first-order matrix phi(Pi). If SCAN succeeds, it computes a first-order formula psi which is equivalent to exists P1...Pn phi(Pi), but does no longer contain the predicate variables Pi any more.

Universally quantified predicate variables can be eliminated by negating the formula first, applying SCAN, and negating the result.

The basic idea of SCAN has already been published in early papers of Ackermann and later on by Kreisel and Krivin: A predicate Pis no longer necessary in a formula set, if this set contains all consequences of the formulae containing P. Of course this set of consequences is usually infinite. Therefore this is not an implementable criterion. But it turns out that a minimal set of relevant consequences is sufficient, and this set may be the set of resolvents with P.

To get a more concrete idea about how SCAN works, consider the following equivalence

(exists P ((P v Q) & (-P v R))) <-> (Q v R)

The right hand side (Q v R) is the resolvent of the two clauses in the left hand side. Therefore the `->' part of the equivalence is trivial. In order to prove the `<-' part, suppose Q v R is true. If Q is true then we choose P to be false. This makes the left hand side true. If Q is false, R must be true. Then we choose P to be true. This again makes the left hand side true. For this argument it is important that P is existentially quantified.

A first version of SCAN can be derived from this observation: Generate all resolvents with the predicates to be eliminated and then keep only the resolvents without these predicates. According to this recipe, we find for example the following equivalence:

(exists P ((P v Q) & (-P v R) v (-P v S))) <-> ((Q v R) & (Q v S))

For propositional variables, this procedure works, terminates always and computes a propositional equivalent. For full predicate logic, we need one extension. Consider the equivalence

(exists P ((P(a) v Q) & (-P(b) v R))) <-> (a = b -> (Q v R))

If a and b are interpreted differently in a model, we can always choose both P(a) and -P(b) to be true. Therefore the left hand side is true in this case. If a and b are interpreted identically, however, we have the same situation as in the propositional example above. Therefore the condition a = b in the resolvent takes care of this possibility. The extension of SCAN to the predicate logic case is now obvious. Instead of unifying the arguments of the resolution literals P(s1,...,s2) and -P(t1,...,t2) we simply generate constraints s1 = t1 & ... &sn = tn =>... as part of the resolvent. The same modification is necessary for the factorization rule.

The structure of the SCAN algorithm is roughly:

Input:: A predicate logic formula and the list of predicates to be eliminated.
Step 1:: Convert the formula into clause normal form (with full Skolemization)
Step 2:: Generate all constraint resolvents and factors with the predicates to be eliminated. Make all equivalence preserving simplifications, such as - elimination of tautologies - elimination of subsumed clauses - unit deletion ( P & (-P v Q)) is equivalent to Q therefore -P can be deleted.) Delete a clause as soon as there is no further resolvent with at least one of the clause's literals (purity deletion)
Step 3:: If step 2 terminates, reconstruct the quantifiers
Output:: Optionally the resulting clause set or the unskolemized formula.

There are two critical points in the algorithm, the resolution loop may not terminate, and the reconstruction of the existential quantifiers from the Skolem functions may not be possible. In the first case, the algorithm simply does not terminate. In the second case there is sometimes a solution in terms of parallel Henkin quantifiers, which are again second-order.

One can show that there cannot be an algorithm which is complete in the sense that it always computes the first-order equivalent if there is some. Otherwise arithmetic would be enumerable. Therefore if SCAN fails to compute a first-order equivalent, this might be an indication, but no guarantee that there is none.

References