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. 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.

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^|)θ

The effect of the ordering constraints is to use the (potentially) largest literal in the from clause (which must be an equality literal), the (potentially) largest side of that equality literal, to paramodulate into the (potentially) largest literal of the into clause. This makes the (potentially) largest literal in the resultant clause smaller than either of the selected literals in its parent, i.e., thyings get smaller. 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,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,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,b)

» q(g(a),c) | p(Y,b) | q(b,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,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,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,b)
g(f(b,b)) is not smaller than c

» g(a) != c | p(Y,b) | q(b,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

`f(a) != Y \| f(X) = c \| p(f(Y),g(X))`	`+`	Equality resolution
`T1 is f(a)` `T2 is Y` `C^\| is f(X) = c \| p(f(Y),g(X))` `θ is {Y/f(a)}`
It must be the case that:		`f(a) != f(a)` is not smaller than `f(X) = c` `f(a) != f(a)` is not smaller than `p(f(f(a)),g(X))`
	»	`f(X) = c \| p(f(f(a)),g(X))`

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(a) | f(X) = c | p(X,d) | ~q(d) + Equality factoring

T1 is f(a)
T2 is b
T3 is f(X)
T4 is c
C^| is p(X,d) | ~q(d)
θ is {X/a}

It must be the case that: b = f(a) is not smaller than f(a) = c
b = f(a) is not smaller than p(a,d)
b = f(a) is not smaller than ~q(d)

» b != c | f(a) = b | p(a,d) | ~q(d)

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.

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'. Then B1 > B2 if for each X2 in B2' there exists a X1 in B1' such that X1 > X2 (the 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).

An optional preordering can be imposed, that all negative literals are larger than positive literals, and then do bag ordering after that.

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) → 2

ω(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)

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.

Example using Ordered Resolution and Superposition

S = { even(sum(two_sq,b)), [14] two_sq = four, [10] ~zero(X) | diff(four,X) = sum(four,X), [26] zero(b), [7] ~even(diff(two_sq,b)) } [13]

ρ : = > even > zero > = > sum > diff > four > two_sq > b

ω(even) → 5

ω(zero) → 5

ω(=) → 3

ω(sum) → 4

ω(diff) → 3

ω(four) → 4

ω(two_sq) → 3

ω(b) → 2

ω(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(two_sq,X) = sum(four,X) [25]

THIS IS BROKEN - INVOKE THE OPTIONAL CONSTRAINT INTO LARGEST LITERAL
+ two_sq = four » ~zero(X) | diff(four,X) = sum(two_sq,X) [25]

~zero(X) | diff(two_sq,X) = sum(four,X) is the ChosenClause

+ two_sq = four » ~zero(X) | diff(two_sq,X) = sum(two_sq,X) [24]

~zero(X) | diff(two_sq,X) = sum(two_sq,X) is the ChosenClause

+ even(sum(two_sq,b)) » ~zero(b) | even(diff(two_sq,b)) [19]

~zero(b) | even(diff(two_sq,b)) is the ChosenClause

+ ~even(diff(two_sq,b)) » ~zero(b) [7]

~zero(b) is the ChosenClause

+ zero(b) » FALSE

Example

S = { ~mother(C,M) | husband_of(M) = father_of(C)]). mother(geoff,maggie), bob = husband_of(maggie), father_of(geoff) != bob }

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 (ignoring the term and literal ordering issues)

S = { a = f(X) | Y = f(b), f(b) = c, a != c }

a = f(X) | Y = f(b) + Equality factoring

» a = f(X) | f(X) != f(b)

a = f(X) | f(X) != f(b) + Equality resolution

» a = f(b)

f(b) = c) + a != c

» a != f(b)

a = f(b) + a != f(b)

» a != a

a != a + Equality resolution

» FALSE

Practical Notes:

Rewriting is really needed to make this effective.
Literal selection strategies, which determine which literal to select, are important.
Without the ordering, superposition is paramodulation, equality factoring is conditional factoring of equality literals and equality resolution is resolution with reflexivity.

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 = true, and a negative literal M is converted to M != true. 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 true. Clauses containing true = true are tautologies and can be discarded.

For the KBO, true 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)) = true, two_sq = four, zero(X) != true | diff(four,X) = sum(four,X), zero(b) = true, even(diff(two_sq,b)) != true }

two_sq = four + even(sum(two_sq,b)) = true

» even(sum(four,b)) = true

zero(X) != true | diff(four,X) = sum(four,X) + even(sum(four,b)) = true

» even(diff(four,b)) = true | zero(b) != true

even(diff(four,b)) = true | zero(b) != true + zero(b) = true

» even(diff(four,b)) = true | true != true

even(diff(four,b)) = true | true != true + Equality resolution

» even(diff(four,b)) = true

even(diff(four,b)) = true + two_sq = four

» even(diff(two_sq,b)) = true

even(diff(two_sq,b)) = true + even(diff(two_sq,b)) != true

» true != true

true != true + Equality resolution

» FALSE

Example

S = { ~mother(C,M) | husband_of(M) = father_of(C)]). mother(geoff,maggie), bob = husband_of(maggie), father_of(geoff) != bob }

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
```

`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^\|)θ`

`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^\|)θ`

`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^\|)θ`