# Resolution Algorithms and one Example Problems?

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?

• @MauroALLEGRANZA is it understandable now? – Sara PhD Jul 21 '16 at 10:47
• See Resolution : "The resolution rule is applied to all possible pairs of clauses that contain complementary literals. After each application of the resolution rule, the resulting sentence is simplified by removing repeated literals. If the sentence contains complementary literals, it is discarded (as a tautology). If not, and if it is not yet present in the clause set S, it is added to S, and is considered for further resolution inferences." 1/2 – Mauro ALLEGRANZA Jul 21 '16 at 11:19
• This is the algorithm "specification"; of course, if applied by a human being, working with insight, it is possible to apply the rule only to the pairs strictly necessary to conclude (if possible). 2/2 – Mauro ALLEGRANZA Jul 21 '16 at 11:21
• @MauroALLEGRANZA Is it possible show works to prove the $6$th clause by clause $1$ to $5$? – Sara PhD Jul 21 '16 at 11:22

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

• I read your answer $10$ times, thanks very nice, but can we say, the clause $2$ is only clause among these $5$ clauses that used more than once in this deduce? – Sara PhD Jul 21 '16 at 21:48
• after your text "Now, we have to apply resolution a first time ..." you only use clause $2$ two times, am I right? – Sara PhD Jul 22 '16 at 8:39
• @SaraPhD - exactly: once with 6') and a second time with 4). – Mauro ALLEGRANZA Jul 22 '16 at 9:03
• so you means non of them is used two times except second clause. Thanks. – Sara PhD Jul 22 '16 at 9:16