How to use resolution in this set?

Question

Exercise: Transform the set of formulas $\{p, p→((q ∨r)∧¬ (q ∧r)), p→((s ∨t)∧¬ (s ∧t )), s→q, ¬r→t, t→s \}$ into clausal form and refute using resolution.

Solution:

Clausal form: $S=\{(1)p,\overline pqr,\overline p\, \overline q\,\overline r,\overline sq,rt,\overline ts,\overline pst,(8)\overline p\,\overline s\,\overline t\}$

Using resolution:

(9) $q\overline t\ $ 4,6

(10) $\overline p\, \overline t\,\overline r\ $ 3,9

(11)$\overline r\overline t\ $ 1,10

(12)$\overline pq\overline t\ $ 11,2

(13)$\overline pqr\ $ 12,5

(14) ?

I'm stuck here since the only available clausal are (7) and (8) but none can be used with (13) i.e. the $\fbox {}$ cannot be derived by (13) with (7) or (8).

What do I do to solve this problem?

Any help for solving this problem is really appreciated.

---

This is the algorithm

Algorithm 4.18 (Resolution procedure) Input: A set of clauses S. Output: S is satisfiable or unsatisfiable. Let S be a set of clauses and define $S_0 = S.$ Repeat the following steps to obtain $S_{i+1}$ from $S_i$ until the procedure terminates as defined below:

• Choose a pair of clashing clauses ${C1,C2} ⊆ S_i$ that has not been chosen before.

• Compute C = Res(C1,C2) according to the resolution rule.

• If C is not a trivial clause, let $S_{i+1} = S_i ∪ {C};$ otherwise, $S_{i+1} = S_i $.

Terminate the procedure if:

• $C =\fbox{} $

• All pairs of clashing clauses have be resolved.

Answer 1

You are stuck because you are under the impression that you can use any clause just once, but that is not true: you can use any clause any number of times.

Also, here is a useful strategy: always try to use clauses that have a single literal if you can. So, for example, since you have clause $p$, resolve that with any of the clauses that have $p'$

Answer 2

Tip: Pick literals in strategic order, or alphabetic, then consecutively resolve all pairs of clauses with conflicts in that literal, until no more unresolved conflicts in that literal remain (or you encounter an empty clause).   Then repeat for the remaining literals.   Thus ensuring that if you don't terminate you will have resolved all conflicting pairs, as the algorithm directs.

Note:

$\{p, p→((q ∨r)∧¬ (q ∧r)), p→((s ∨t)∧¬ (s ∧t )), s→q, ¬r→t, t→s \}$ into clausal form and refute using resolution.

$\{p, (\overline p, q , r), (\overline p, \overline q , \overline r), (\overline p,s,t), (\overline p,\overline s,\overline t), (\overline s,q), (r,t), (\overline t, s) \}$

Clearly the first move is to resolve away all pairs of $p$ vs $\overline p$ conflicts.

Notice: $\{p, (\overline p, q , r)\}, \{p, (\overline p, \overline q , \overline r)\}, \{p, (\overline p,s,t)\}, \{p, (\overline p,\overline s,\overline t)\}$ are all distinct pairs despite containing the same literal.

$\{(q , r), (\overline q , \overline r), (s,t), (\overline s,\overline t), (\overline s,q), (r,t), (\overline t, s) \}$

Alphabetise

$\{(q, r), (q,\overline s),(\overline q,\overline r),(r,t),(s,t),(s,\overline t),(\overline s,\overline t)\}$

Resolve away all the $q$ vs $\overline q$ conflicts

$\{(\overline r,\overline s),(r,t),(s,t),(s,\overline t),(\overline s,\overline t)\}$

Resolve away all the $r$ vs $\overline r$

$\{(\overline s,t),(s,t),(s,\overline t),(\overline s,\overline t)\}$

Resolve those $s$

$\{(t),(\overline t)\}$

Which is more clearly a contradiction, but resolve to an empty clause anyway.

$\{()\}$