Resolution Algorithms and one Example Problems?

Question

We have a problem in one Resolution question.

There is $5$ clauses, and want to prove the $6$th clause is true. which of the following clause is need more than one times to prove $6$th clause? $t$ to $z$ be variables, $A$ to $C$ is constant values, $f$ be function, $D$ and $E$ are predicates.

---

$1) \neg E(t, u) \lor E(u, t)$

$2) \neg D(v, w) \lor E(f(v), w)$

$3) \neg E(x, y) \lor \neg E(y, z) \lor E(x, z)$

$4) D(A, C)$

$5) \neg E(C, B)$

$6) \neg D(A, B)$

---

The solution is option $2$ (i.e The clause $2$ is used more that one times for proving the $6$th clause is true).

my question is about solving this problems, is there anyway to quickly get this answer? or we should completely solve it? any idea for getting this solution?

Answer 1

To prove 6) from 1)-5), by Resolution, we have to add to 1)-5) its negation:

6') $D(A, B)$.

Then we need Unification.

Performing the following substitution:

$A \to v, \ B \to z,\ C \to u, x, \ f(A) \to t, y$

we get:

$1) \neg E(f(A), C) \lor E(C, f(A))$

$2) \neg D(A, w) \lor E(f(A), w)$

$3) \neg E(C, f(A)) \lor \neg E(f(A), B) \lor E(C, B)$

$4) D(A, C)$

$5) \neg E(C, B)$

$6') D(A, B)$.

Now, we have to apply resolution a first time with 6') and 2), with $B \to w$, to get :

7) $E(f(A),B)$

and a second time with 4) and 2), with $C \to w$, to get :

8) $E(f(A), C)$.

Using now 1) and 8) we get:

9) $E(C, f(A))$.

Finally, 9), 7) and 3) will get:

10) $E(C,B)$

that, with 5), will produce the sought contradiction.

---

Comment : this is a case where the "original" formulae are more easily managed...

The clause 2) is derived from :

$\forall v \ \forall w \ [D(v, w) \to E(f(v), w)]$;

thus, "instantiating" twice with $A,B$ and $A,C$ respectively, gives:

$D(A, B) \to E(f(A), B)$

and

$D(A, C) \to E(f(A), C)$,

that are "well-fitted" for modus ponens with 4) and 6').