Example |
---|
two_squared = four ∀X (zero(X) => difference(four,X) = sum(four,X)) zero(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)) }
|
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:
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) }
|
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.
Example | ||||||
---|---|---|---|---|---|---|
|
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 | ||||||
---|---|---|---|---|---|---|
|
Example | |||
---|---|---|---|
|
Example | |||
---|---|---|---|
|
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.
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.
Depending on how paramodulation is used, it is often unnecessary to paramodulate from variables. In the definition above, this constrains T1 and T2 to be non-variables. I MUST CHECK OUT THE DETAILS OF THIS.
Another pragmatic refinement is never paramodulate both ways (from and into) between two positive equality literals - the result is the same both ways, so only one is necessary.
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 }
|
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).
S = { p(f(a)), a = c, ~q(W,W) | f(c) = f(d), q(b,b) }
~p(X,Y) | ~q(Y) | f(X) = g(c,Y) p(f(a),g(Z,b)) | q(Z) | g(c,c) = c