Superposition
Superposition is a paramodulation-like inference rule, with constraints based on orderings on
the terms and equality literals.
Equality resolution and equality factoring are combined with superposition to form a complete
inference system for pure equality problems - problems expressed using only equality.
Let T1 = T2 represent also T2 = T1.
Then ...
| T1 = T2 | C|
| +
| L[TT] | D|
|
|
|
T1θ ≡ TTθ
|
|
|
(T1 = T2)θ is not smaller than any literal in
(T1 = T2 | C|)θ
|
|
|
T1θ is not smaller than T2θ in the term ordering
|
|
|
Lθ is not smaller than any literal in
(L | D|)θ
|
|
| »
| (L[T2] | C| | D|)θ
|
Note that the tests are being done after the subsitutions required for the inference, to
maximise the effect (see Ordering).
The effect of the ordering constraints is to use literals in the from clause (which must be
equality literals) that are not known to be smaller than any other literal in the clause, the
side of that equality literal that is not known to be smaller than the other side, to
paramodulate into literals of the into clause that are not known to be smaller than any other
literal in the clause.
The literals in the resultant clause are smaller than the selected literals in its parent.
As the ordering is well founded, this cannot go on for ever.
Example
| a = f(X,b) | p(Y,X)
| +
| q(g(f(b,Z)),c) | q(Z)
|
T1 is f(X,b)
T2 is a
C| is p(Y,X)
|
| L is q(g(f(b,Z)),c)
TT is f(b,Z)
D| is q(Z)
|
| θ is {X/b, Z/b}
|
| It must be the case that:
|
| a = f(b,b) is not smaller than p(Y,b)
f(b,b) is not smaller than a
q(g(f(b,b)),c) is not smaller than q(b)
|
|
| »
| q(g(a),c) | p(Y,b) | q(b)
|
|
|---|
If L is an (in)equality literal, then a tighter constraint may be imposed.
Let ·= mean = or !=, i.e., T1 ·= T2 means any of
T1 = T2, T2 = T1, T1 != T2, T2 != T1.
Then ...
| T1 = T2 | C|
| +
| T3[TT] ·= T4 | D|
|
|
|
T1θ ≡ TTθ
|
|
|
(T1 = T2)θ
is not smaller than any literal in
(T1 = T2 | C|)θ
|
|
|
T1θ
is not smaller than
T2θ
in the term ordering
|
|
|
(T3 ·= T4)θ
is not smaller than any literal in
(T3 ·= T4 | D|)θ
|
|
|
T3θ
is not smaller than
T4θ
in the term ordering
|
|
| »
| (T3[T2] ·= T4 | C| | D|)θ
|
Example
| a = f(X,b) | p(Y,X)
| +
| g(f(b,Z)) != c | q(Z)
|
T1 is f(X,b)
T2 is a
C| is p(Y,X)
|
| T3 is g(f(b,Z))
T4 is c
TT is f(b,Z)
D| is q(Z)
|
| θ is {X/b, Z/b}
|
| It must be the case that:
|
| a = f(b,b) is not smaller than p(Y,b)
f(b,b) is not smaller than a
g(f(b,b)) != c is not smaller than q(b)
g(f(b,b)) is not smaller than c
|
|
| »
| g(a) != c | p(Y,b) | q(b)
|
|
|---|
Equality Resolution and Equality Factoring
| T1 != T2 | C|
| +
| Equality resolution
|
|
|
T1θ ≡ T2θ
|
|
|
(T1 != T2)θ
is not smaller than any literal in
(T1 != T2 | C|)θ
|
|
| »
| C|θ
|
Example
| g(f(a)) != g(Y) | p(f(Y),g(c))
| +
| Equality resolution
|
T1 is g(f(a))
T2 is g(Y)
C| is p(f(Y),g(c))
θ is {Y/f(a)}
|
|
|
| It must be the case that:
|
| g(f(a)) != g(f(a)) is not smaller than p(f(f(a)),g(c))
|
|
| »
| p(f(f(a)),g(c))
|
|
|---|
| T1 = T2 | T3 = T4 | C|
| +
| Equality factoring
|
|
|
T1θ ≡ T3θ
|
|
|
(T1 = T2)θ
is not smaller than any literal in
(T1 = T2 | T3 = T4 | C|)θ
|
|
| »
| (T2 != T4 | T1 = T2 | C|)θ
|
Example
| b = f(X) | f(a) = c | p(X,d)
| +
| Equality factoring
|
T1 is f(X)
T2 is b
T3 is f(a)
T4 is c
C| is p(X,d)
θ is {X/a}
|
|
|
| It must be the case that:
|
| b = f(a) is not smaller than f(a) = c or p(a,d)
|
|
| »
| b != c | f(a) = b | p(a,d)
|
|
|---|
Without the ordering, superposition is paramodulation, equality factoring is conditional
factoring of equality literals and equality resolution is resolution with reflexivity.
Term and Literal Ordering
Superposition requires a ground completable reduction ordering on the terms.
Superposition can also use a ground completable simplification ordering, which is even stronger.
Knuth-Bendix Ordering provides a suitable term
ordering.
Additionally, superposition requires an ordering on the literals of clauses, with some special
cases:
- An equality literal is represented by its largest argument.
- A negative literal is greater than a positive literal with the equivalent atom (seen that
before!).
A literal ordering extends a term ordering to literals, and must also be stable under substitution
and renaming.
An example of a literal ordering that can be used with superposition is bag ordering:
Given two bags, B1 and B2:
- Discard pairs of identical elements taken one from each bag, to produce
B1' and B2'.
- B1 > B2 if for each X2 in B2' there exists a
X1 in B1' such that X1 > X2 (by KBO for terms, by
bag ordering for nested bags).
- Any X1 can be used for multiple X2s.
Literals are compared by bag-comparing representative bags:
- A positive non-equality literal L is represented by a bag {{L}} (a bag of
a bag of the atom)
- A negative non-equality literal ~L is represented by a bag {{L,L}} (a bag
of a bag of two copies of the atom - the effect is to make negative literals bigger than
positive ones)
- A positive equality literal T1 = T2 is represented by a bag {{T1},{T2}}
(a bag of two bags, each containing one term)
- A negative equality literal T1 != T2 is represented by a bag {{T1,T2}}
(a bag containing one bag, containing both terms).
| Example
|
|---|
S = { even(sum(two_sq,b)),
two_sq = four,
~zero(X) | diff(four,X) = sum(four,X),
zero(b),
~even(diff(two_sq,b)) }
ρ: even > zero > = > sum > diff > four > two_sq > b
| ω(even)
| →
| 5
|
| ω(zero)
| →
| 5
|
| ω(=)
| →
| 3
|
| ω(sum)
| →
| 4
|
| ω(diff)
| →
| 3
|
| ω(four)
| →
| 4
|
| ω(two_sq)
| →
| 3
|
| ω(b)
| →
| 3
|
| ω(X)
| →
| 1
|
| ~zero(X)
| →
| {{zero(X),zero(X)}}
|
| diff(four,X) = sum(four,X)
| →
| {{diff(four,X)},{sum(four,X)}}
|
|
|
| diff(four,X)
| >
| zero(X)
|
| ... therefore ...
|
| {diff(four,X)}
| >
| {zero(X),zero(X)}
|
| ... therefore ...
|
| {{diff(four,X)},{sum(four,X)}}
| >
| {{zero(X),zero(X)}}
|
| ... therefore ...
|
| diff(four,X) = sum(four,X)
| >
| ~zero(X)
|
|
Therefore that literal is used, and sum(four,X) must be
the chosen term for superposition.
|
|
Superposition+ER+EF is used in conjunction with other inference rules.
For example, superposition+ER+EF combined with resolution forms a refutation complete system in
which there is no need to resolve on equality literals.
The resolution can be ordered using the superposition ordering for literal selection, so that in
each parent of every inference only the largest literals are used.
| Example using Ordered Resolution and Superposition
|
|---|
S = { even(sum(two_sq,b)), [15]
two_sq = four, [9]
~zero(X) | diff(four,X) = sum(four,X), [26]
zero(b), [8]
~even(diff(two_sq,b)) } [14]
ρ : even > zero > = > sum > diff > four > two_sq > b
| ω(even)
| →
| 5
|
| ω(zero)
| →
| 5
|
| ω(=)
| →
| 3
|
| ω(sum)
| →
| 4
|
| ω(diff)
| →
| 3
|
| ω(four)
| →
| 4
|
| ω(two_sq)
| →
| 3
|
| ω(b)
| →
| 3
|
| ω(X)
| →
| 1
|
| zero(b)
|
| is the ChosenClause
|
| two_sq = four
|
| is the ChosenClause
|
| ~even(diff(two_sq,b))
|
| is the ChosenClause
|
| even(sum(two_sq,b))
|
| is the ChosenClause
|
| ~zero(X) | diff(four,X) = sum(four,X)
|
| is the ChosenClause
|
|
| +
| two_sq = four
| »
| ~zero(X) | diff(four,X) = sum(two_sq,X) [25]
|
| ~zero(X) | diff(four,X) = sum(two_sq,X)
|
| is the ChosenClause
|
|
| +
| even(sum(two_sq,b))
| »
| ~zero(b) | even(diff(four,b)) [23]
|
| ~zero(b) | even(diff(four,b))
|
| is the ChosenClause
|
|
| +
| two_sq = four
| »
| ~zero(b) | even(diff(two_sq,b)) [22]
|
| ~zero(b) | even(diff(two_sq,b))
|
| is the ChosenClause
|
|
| +
| ~even(diff(two_sq,b))
| »
| ~zero(b) [8]
|
| ~zero(b)
|
| is the ChosenClause
|
|
| +
| zero(b)
| »
| FALSE
|
|
An optional preordering can be imposed, that all positive literals are smaller than negative
literals, and then do bag ordering after that.
(Try the above example with this added constraint.)
| Example
|
|---|
S = { ~mother(C,M) | husband_of(M) = father_of(C),
mother(geoff,maggie),
bob = husband_of(maggie),
father_of(geoff) != bob }
|
Pure Equality Problems
| Example
|
|---|
S = { a = f(X) | b = f(b), [15]
f(b) = c, [8]
a != c [6]
b != c } [6]
ρ : alphabetic
ω : non-variables → 2; variables → 1.
| a != c
|
| is the ChosenClause
|
| b != c
|
| is the ChosenClause
|
| f(b) = c
|
| is the ChosenClause
|
| a = f(X) | b = f(b)
|
| is the ChosenClause
|
|
| +
| Equality factoring
| »
|
|
| COMPLETE THIS (see my sheet in notes)
|
|
Practical Notes:
- Don't do substitutions between positive literals both ways - it's redundant.
- Rewriting is really needed to make this effective.
Transforming Not Pure Equality Problems
Problems that use predicates other than =/2 and !=/2 can be converted to pure
equality, so that they can be solved using superposition plus equality resolution and factoring.
A positive literal L is converted to L = eqTrue, and a negative literal M
is converted to M != eqTrue.
In this manner all predicate symbols become function symbols.
In the use of the inference rules it is necessary to ensure that no variable becomes instantiated
to (what was previously) an atom, or to the new special constant eqTrue.
Clauses containing eqTrue = eqTrue are tautologies and can be discarded.
For the KBO, eqTrue is mapped to something less than all other symbols and greater
than the mapping of the variables.
| Example
|
|---|
S = { even(sum(two_sq,b)),
two_sq = four,
~zero(X) | diff(four,X) = sum(four,X),
zero(b),
~even(diff(two_sq,b)) }
... gets converted to ...
S = { even(sum(two_sq,b)) = eqTrue, [20]
two_sq = four, [10]
zero(X) != eqTrue | diff(four,X) = sum(four,X), [31]
zero(b) = eqTrue, [13]
even(diff(two_sq,b)) != eqTrue } [19]
ρ: even > zero > = > sum > diff > four > two_sq > b > eqTrue
| ω(even)
| →
| 5
|
| ω(zero)
| →
| 5
|
| ω(=)
| →
| 3
|
| ω(sum)
| →
| 4
|
| ω(diff)
| →
| 3
|
| ω(four)
| →
| 4
|
| ω(two_sq)
| →
| 3
|
| ω(b)
| →
| 3
|
| ω(eqTrue)
| →
| 2
|
| ω(X)
| →
| 1
|
| two_sq = four
|
| is the ChosenClause
|
|
| +
| two_sq = four
|
|
| Example
|
|---|
S = { ~mother(C,M) | husband_of(M) = father_of(C)]).
mother(geoff,maggie),
bob = husband_of(maggie),
father_of(geoff) != bob }
|
Exam Style Questions
- List all the possible superposition and ordered resolution results
of the following two clauses.
Use KBO bag ordering with predicates and functions weighted 2, variables
weighted 1, and alphabetic symbol ordering.
~p(X,Y) | ~q(Y) | f(X) = g(c,Y)
p(f(a),g(Z,b)) | q(Z) | g(c,c) = c