0

I've been tasked with resolving the following statement to prove that it is valid:

$(p\rightarrow q) \rightarrow ((p \lor r) \rightarrow (q \lor r))$

I convert to CNF with the following set of clauses as a result:

$\{\{p, \lnot p, q, r\}, \{\lnot q, \lnot p, q, r\}, \{p, \lnot r, q, r\}, \{\lnot q, \lnot r, q, r\}\}$

I've labelled them (1) through (4) when applying the resolution steps.

When I attempt to resolve by refutation, I hit a bit of a wall; when applying the rule to most of these, I eliminate the resolvent because it's the trivial clause - so it's not added to the set of clauses. However, at some point, I always come across a non-trivial resolvent, namely $\{\lnot p, q, r\}$ when resolving on (1) and (2). This is then labelled (5) added to the set to give:

$\{\{p, \lnot p, q, r\}, \{\lnot q, \lnot p, q, r\}, \{p, \lnot r, q, r\}, \{\lnot q, \lnot r, q, r\}, \{\lnot p, q, r\}\}$

I've redone this step several times, with different combinations of the above clauses but always end up with the final resolvent of $\{\lnot p, q, r\}$. Though, since the statement is a tautology, it should resolve to the empty set of clauses.

Is my CNF conversion possibly the problem, or am I missing something in the resolution step?

Mauro ALLEGRANZA
  • 94,169
Zenadia Groenewald
  • 13
  • I don't know the notation of the "resolution refutation" method which you want to use. However, in your CNF form you have either $p\vee \neg p$, $q\vee \neg q$ or $r\vee \neg r$ in each clause, thus it should be clear from that fact that the statement is valid. – Ove Ahlman Jun 30 '16 at 06:42
  • See Resolution: " If the sentence contains complementary literals, it is discarded (as a tautology)." – Mauro ALLEGRANZA Jun 30 '16 at 07:24
  • Typically, yes, you'd exclude those trivial clauses when writing in CNF. In resolution refutation, however, you don't (unless I have it wrong). If there is exactly one contradicting literal, you resolve it and add the resulting clause to the set of clauses. If there is more than one, you can still resolve, but then you just don't add the resulting clause to the set of clauses. – Zenadia Groenewald Jun 30 '16 at 07:25
  • I have the resolution rule described here as the following: "Resolution is only performed if the pair of clauses clash on exactly one pair of complementary literals. If two clauses clash on more than one literal, their resolvent is a trivial clause. It is not strictly incorrect to perform resolution on such clauses, but since trivial clauses contribute nothing to the satisfiability/unsatisfiability of the set of clauses, we agree to delete them from the set and not perform resolution on clauses with two clashing pairs of literals." – Zenadia Groenewald Jun 30 '16 at 07:30
  • Is it strictly necessary to remove all trivial clauses from the set before resolving, or can it be resolved even if they are included in the set of clauses? – Zenadia Groenewald Jun 30 '16 at 07:31
  • You have to take into account that the set of clauses is nothing more than $D_1 \land D_2 \land \ldots \land D_n$, where each $D_i$ is a disjunction. The tautological equivalences still hold; thus, due to the fact that $p \lor \lnot p \equiv TRUE$ and $TRUE \lor A \equiv TRUE$, every disjunct with one (or more) couple of complementary literls must be replaced by $TRUE$. But $TRUE \land B \equiv B$ and thus any disjunct (i.e. clause) $D_i$ with one (or more) couple of complementary literals can be deleted without affecting the satisfiability of the initial set of clauses. – Mauro ALLEGRANZA Jun 30 '16 at 09:10

1 Answers1

2

To show that the formula:

$(p→q)→((p∨r)→(q∨r))$

is valid with Resolution, we have to consider its negation and show that this is unsatisfiable.

Thus, we have to consider:

$\lnot [\lnot (\lnot p ∨ q) ∨ (\lnot (p∨r) ∨ (q∨r))]$

i.e.

$(\lnot p ∨ q) \land (p∨r) \land \lnot q \land \lnot r)$.

Thus, we have the set of clauses:

$\{ \{ ¬p,q \}, \{ p,r \}, \{ ¬q \}, \{ ¬r \} \}$.

As you can verify, we can derive the empty clause, showing that the set of clauses is unsatisfiable, and thus that the initial formula is a tautology.

Mauro ALLEGRANZA
  • 94,169