Some concrete questions about resolution method for predicate logic

Question

I think I understand the basics of it now, and when I practice on excersices and old exams it goes well most of the time. But I have some questions that I cant seem to find any straight forward answers to and it would help me so much if someone could help me out.

1. In this picture enter image description here of an example I found he is using several "paths" and then he connects them. Is that something you can allways do? And am I right about that you can do it in several ways, so with only one path in this case?
2. I asked this in another thread but I think it got too messy, because no one really answered. But is it so that you dont have to use all the formulas in the resolution as long as you finish with an empty clause? For example if in the picture the solution had q(x) and -p(x) seperately, its enough to use one of them and in other words he could have taken p(a) against -p(x) and thats it?

Answer 1

See Resolution (logic) :

The resolution technique uses proof by contradiction.

The resolution rule is applied to all possible pairs of clauses that contain complementary atoms. 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, it is added to it, and is considered for further resolution inferences.

If after applying a resolution rule the empty clause is derived, the original formula is unsatisfiable (or contradictory), and hence it can be concluded that the purported conclusion follows from the premises.

In your example, after the initial transformations, unification is performed, substituting $a$ for $x$ in the clauses $\lnot p(x) \lor q(x)$ and $\lnot p(x) \lor \lnot q(x) \lor r(x)$.

What we get is a new set of clauses :

1) $\lnot p(a) \lor \lnot q(a) \lor r(a)$

2) $p(a)$

3) $\lnot r(a)$

4)$\lnot p(a) \lor q(a)$.

Now we apply the Resolution rule "to all possible pairs of clauses that contain complementary atoms."

What we get is :

5) $\lnot q(a) \lor r(a)$ --- from 1) and 2)

6) $q(a)$ --- from 2) and 4)

7) $\lnot q(a)$ --- from 3) and 5).

Now we can stop, because applying the Resolution rule again to clauses 6) and 7) we get the empty clause.

What is the empty clause ? It is obtained conjoining to complementary atoms : $q(a)$ and $\lnot q(a)$.

But this amounts to $q(a) \land \lnot q(a)$, which is a contradiction. Thus, the empty clause is simply a contradicition.

Having found a contradicition, the Resoultion algorithm proves that the original set of clauses is unsatisfiable, that means that the conclusion is implied by the premises.

Regarding :

you dont have to use all the formulas in the resolution as long as you finish with an empty clause?

the answer is : you dont.

The procedure is an algorithm, suitable for mechanized execution. Thus, the rule is : "apply the rule to all possible ..."

But when we humans use it, we are guided by our understanding of the problem, and thus we can choose to perform only the steps necessary to derive the empty clause.