SCAN
The Theory
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.
SCAN Home
Forms:
Basic Form |
Correspondences Form |
Circumscription Form |
Help
Documentation:
Theory |
Computing Correspondences |
Computing Circumscription |
The System |
Conventions |
Syntax |
Literature
Maintained by
schmidt@cs.man.ac.uk.
Last modified: 05 Aug 13