Equality

Many domains require the use of the notion of equality. In 1st order logic equality statements use the infix =/2 and !=/2 predicates.

Example

Axioms
even(sum(two_squared,b)) two_squared = four ∀X (zero(X) => difference(four,X) = sum(four,X)) zero(b)

Conjecture
even(difference(two_squared,b))

Example
Axioms `even(sum(two_squared,b)) two_squared = four ∀X (zero(X) => difference(four,X) = sum(four,X)) zero(b)` Conjecture `even(difference(two_squared,b))`

Although the conjecture may seem like a logical consequence to humans, that's because humans "know" what equal means (even without knowing what the "maths" means). One can use ones intuitive understanding of equality in a resolution refutation.

Example

S = { even(sum(two_squared,b)), two_squared = four, ~zero(X) | difference(four,X) = sum(four,X), zero(b), ~even(difference(two_squared,b)) }

even(sum(two_squared,b)) + two_squared = four

» even(sum(four,b))

~zero(X) | difference(four,X) = sum(four,X) + zero(b)

» difference(four,b) = sum(four,b)

even(sum(four,b)) + difference(four,b) = sum(four,b)

» even(difference(four,b))

even(difference(four,b)) + two_squared = four

» even(difference(two_squared,b)

~even(difference(two_squared,b)) + even(difference(two_squared,b)

» FALSE

However, there are models of the axioms that are not a models of the conjecture:

Example

D = { cat, dog } F = { b → cat, two_squared → cat, four → cat, difference(cat,cat) → dog, difference(cat,dog) → cat, difference(dog,cat) → cat, difference(dog,dog) → cat, sum(cat,cat) → cat, sum(cat,dog) → cat, sum(dog,cat) → cat, sum(dog,dog) → cat } R = { even(cat) → TRUE, even(dog) → FALSE, cat = cat → TRUE, cat = dog → FALSE, dog = cat → TRUE, dog = dog → FALSE, zero(cat) → TRUE, zero(dog) → FALSE }

Example
D = { cat, dog } F = { b → cat, two_squared → cat, four → cat, difference(cat,cat) → dog, difference(cat,dog) → cat, difference(dog,cat) → cat, difference(dog,dog) → cat, sum(cat,cat) → cat, sum(cat,dog) → cat, sum(dog,cat) → cat, sum(dog,dog) → cat } R = { even(cat) → TRUE, even(dog) → FALSE, cat = cat → TRUE, cat = dog → FALSE, dog = cat → TRUE, dog = dog → FALSE, zero(cat) → TRUE, zero(dog) → FALSE }

Such models are possible because the axioms are missing definitions for equality. These definitions are the axioms of equality, and must be included to force equality to have its usual meaning. They are:

Reflexivity - everything equals itself
Symmetry - If X equals Y then Y equals X
Transitivity - If X equals Y and Y equals Z, then X equals Z

∀X (X = X)
∀X ∀Y (X = Y => Y = X)
∀X ∀Y ∀Z ((X = Y & Y = Z) => X = Z)

Function substitution - If X equals Y then f(X) equals f(Y). For every argument position of every functor.
Predicate substitution - If X equals Y and p(X) is TRUE, then p(Y) is TRUE For every argument position of every predicate.

∀X ∀Y ∀Z (X = Y => sum(X,Z) = sum(Y,Z))
∀X ∀Y ∀Z (X = Y => sum(Z,X) = sum(Z,Y))
∀X ∀Y ∀Z (X = Y => difference(X,Z) = difference(Y,Z))
∀X ∀Y ∀Z (X = Y => difference(Z,X) = difference(Z,Y))
∀X ∀Y ((X = Y & even(X)) => even(Y))
∀X ∀Y ((X = Y & zero(X)) => zero(Y))

With these axioms, it is possible to expand the example to a complete resolution refutation.

Example

S = { even(sum(two_squared,b)), two_squared = four, ~zero(X) | difference(four,X) = sum(four,X), zero(b), ~even(difference(two_squared,b)), X = X, X != Y | Y = X, X != Y | Y != Z | X = Z, X != Y | sum(X,Z) = sum(Y,Z), X != Y | sum(Z,X) = sum(Z,Y), X != Y | difference(X,Z) = difference(Y,Z), X != Y | difference(Z,X) = difference(Z,Y), X != Y | ~even(X) | even(Y), X != Y | ~zero(X) | zero(Y) }

even(sum(two_squared,b)) + X != Y | ~even(X) | even(Y)

» sum(two_squared,b) != Y | even(Y)

sum(two_squared,b) != Y | even(Y) + X != Y | sum(X,Z) = sum(Y,Z)

» two_squared != Y | even(sum(Y,b))

two_squared != Y | even(sum(Y,b) + two_squared = four

» even(sum(four,b))

~zero(X) | difference(four,X) = sum(four,X) + zero(b)

» difference(four,b) = sum(four,b)

even(sum(four,b)) + X != Y | ~even(X) | even(Y)

» sum(four,b) != Y | even(Y)

sum(four,b) != Y | even(Y) + X != Y | Y = X

» Y != sum(four,b) | even(Y)

Y != sum(four,b)) | even(Y) + difference(four,b) = sum(four,b)

» even(difference(four,b))

even(difference(four,b)) + X != Y | ~even(X) | even(Y)

» difference(four,b) != Y | even(Y)

difference(four,b) != Y | even(Y) + X != Y | difference(X,Z) = difference(Y,Z)

» four != Y | even(difference(Y,b))

four != Y | even(difference(Y,b)) + X != Y | Y = X

» Y != four | even(difference(Y,b))

Y != four | even(difference(Y,b)) + two_squared = four

» even(difference(two_squared,b)

~even(difference(two_squared,b)) + even(difference(two_squared,b)

» FALSE

Example (you fill in the equality axioms)

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

Example (you fill in the equality axioms)
S = { ~mother(C,M) \| husband_of(M) = father_of(C), mother(geoff,maggie), bob = husband_of(maggie), father_of(geoff) != bob }

The general problem is to show that two atoms can be made unifiable, by virtue of a sequence of resolution steps with equality axioms and other equalities.

Paramodulation

Paramodulation is an inference rule generates all "equal" versions of clauses, modulo conditions on the equality information.

Example

live_in_uk => ruler = king P+ idiot(king)

» live_in_uk => idiot(ruler)

The paramodulation operation takes two parent clauses, the from clause and the into clause. The from clause must contain a positive equality literal. One of the equality literal's arguments must unify with a subterm in the into clause. After unification of the argument and the subterm, the subterm is replaced by the other argument of the equality literal. The literals of the from clause, except the equality literal, and the literals of the into clause are disjoined to form the paramodulant.

T1 = T2 | C^| + D[T3]

T1θ=T3θ

» (C^| | D[T2])θ

or

T2θ=T3θ

» (C^| | D[T1])θ

Paramodulation replaces equal subterms in clauses. One subterm is replaced at a time; multiple paramodulation steps can be used to do multiple replacements.

Example

~live_in_uk | ruler = king P+ idiot(king)

» ~live_in_uk | idiot(ruler)

Example

f(X,a) = g(X) | p(X,b) | q(c) P+ r(S) | ~q(g(f(b,S)))

Paramodulation does the job of all the equality axioms except reflexivity, which must be added to the input. Use paramodulation alongside resolution, but there is no need to resolve on equality literals except against reflexivity.

Restrictions

Never paramodulate into variables, i.e., it is never necesary to replace a variable subterm by a non-variable equality literal argument. As the general aim of paramodulation is to make atoms unifiable, replacing a variable with a term will not help. If the variable later becomes instantiated to a "unsuitable" subterm, paramodulation can then replace that subterm. In the definition above, this constrains T3 to be a non-variable.
Never paramodulate both ways (from and into) between two positive equality literals - the result is the same both ways, so only one is necessary.
Depending on how paramodulation is used, it is often unnecessary to paramodulate from variables. I MUST CHECK OUT THE DETAILS OF THIS. In the definition above, this constrains T1 and T2 to be non-variables. In particular, it is never necessary to paramodulate from the reflexivity axiom - use only for resolution.

Example

p(X,Y) | f(X) = g(a) P+ g(Z) = Z | p(g(Z),f(b)) | q(f(a))

Example

S = { even(sum(two_squared,b)), two_squared = four, ~zero(X) | difference(four,X) = sum(four,X), zero(b), ~even(difference(two_squared,b)), X = X }

even(sum(two_squared,b)) P+ two_squared = four

» even(sum(four,b))

~zero(X) | difference(four,X) = sum(four,X) + zero(b)

» difference(four,b) = sum(four,b)

even(sum(four,b)) P+ difference(four,b) = sum(four,b)

» even(difference(four,b))

even(difference(four,b)) P+ two_squared = four

» even(difference(two_squared,b)

~even(difference(two_squared,b)) + even(difference(two_squared,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 }

One of the problems with paramodulation is that it is pre-emptive. It generates all equal variants of clauses without knowing which of the variants will be useful. This motivates the superposition rule, which is better (but more complicated).

Exam Style Questions

What axioms of equality should be added to the following clause set?

S = { p(f(a)),
      a = c,
      ~q(W,W) | f(c) = f(d),
      q(b,b) }

List all the possible paramodulants of the following two clauses (no paramodulation into variables):
```
~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^\|`	`+`	`D[T3]`
	`T1θ=T3θ`
	»	`(C^\| \| D[T2])θ`
or
	`T2θ=T3θ`
	»	`(C^\| \| D[T1])θ`