Equality

Many domains require the use of the notion of equality. In 1st order logic equality statements use the prefix equal/2 predicate, or 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))

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 }

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:

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

∀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)
is 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 }

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 equality

Paramodulation

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

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
p(X,Y) | f(X) = g(a)  P+  g(Z) = Z | p(g(Z),f(b)) | q(f(a))

It is never necessary to paramodulate into variables, i.e, it is never necesary to replace a variable subterm by a non-variable equality literal argument, using paramodulation. 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. Similarly, depending on how paramodulation is used, it is often unnecessary to paramodulate from variables, i.e., it is often unnecessary to a paramodulation where one of the equality literal's arguments is a variable, and that variable is unified with the subterm which is then replaced. In the definition above, this constrains T1 and T2 to be non-variables. I MUST CHECK OUT THE DETAILS OF THIS.

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 }

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.

Exam Style Questions

  1. 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) }
  2. 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