How to use resolution to prove a sentence is unsatisfiable?

I need to use resolution to prove this sentence is unsatisfiable. $(p\lor q \lor \neg r) \land ((\neg r \lor q \lor p) \to((r \lor q) \land \neg q \land \neg p))$ . My clausal form is this. $\<< p, q, \neg r\>>$ $\$ . With resolution, I know that if you have something like $\$ and $\$ then the negations would cancel out but you can only do one at a time so you'd get both $\$ and $\$ . Do you do the same thing with a clause of 3? So for my example, if I start by cancelling out $r$ and $\neg r$ then would I get $\$ ? The problem with this is that I started doing this and I'm up to 27 lines and I cannot see how I can possibly derive the empty clause. So am I doing something wrong with my resolution or is my clausal form wrong altogether?

$\begingroup$ Unless I'm misreading something, your sentence is satisfiable, by making $r$ true and making both $p$ and $q$ false. Then the first conjunct, $p\lor q\lor r$ is true because of the disjunct $r$. The second conjunct is an implication that is true because its antecedent $\neg r\lor q\lor p$ is false. (Are you sure you transcribed the sentence correctly?) $\endgroup$

$\begingroup$ It seems as though the first conjunct was transcribed incorrectly, and the conditional was transformed incorrectly ( into disjuncts where it should have been conjuncts ). $\endgroup$

2 Answers 2

The statement $(p\lor q \lor r) \land ((\neg r \lor q \lor p) \to((r \lor q) \land \neg q \land \neg p))$ cannot be satisfied if-and-only-if the clausal form may be resolved to emptiness.

So the first task is to place the statement in CNF, mainly involving transforming that conditional. $$(\neg r \lor q \lor p) \to((r \lor q) \land \neg q \land \neg p)\\ (r\land \lnot p\land\lnot q)\lor(r\land\lnot q\land \lnot p)\\r\land\lnot p\land\lnot q$$

So the clausal form for the original statement is $\, \,\<\lnot q\>,\<\lnot p\>\>$ which almost immediately resolves down to $\<\,\<\lnot q\>,\<\lnot p\>\>$ .

So, it seems the clausal form may not be resolved to emptiness since $r,\lnot p, \lnot q$ does satisfy the statement.

PS: the statement $(p\lor q \lor\lnot r) \land ((\lnot r \lor q \lor p) \to((r \lor q) \land \lnot q \land \lnot p))$ cannot be satisfied, because it's clausal form is $\, \,\<\lnot q\>,\<\lnot p\>\>$ .

Something went wrong here.

First of all, as Andres points out in the comments, the sentence you give is perfectly satisfiable.

Second, given that your initial sentence is a conjunction, one of which is $p \land q \land r$ , the clause $\< p, q, r \>$ should appear . unless it is absorbed by some other clause, but your clauses don't absorb it.

OK, so let's take your sentence and put it in CNF:

$(p\lor q \lor r) \land ((\neg r \lor q \lor p) \to((r \lor q) \land \neg q \land \neg p)) \overset<\Leftrightarrow>$

$(p\lor q \lor r) \land (\neg (\neg r \lor q \lor p) \lor(r \land \neg q \land \neg p)) \overset<\Leftrightarrow>$

$(p\lor q \lor r) \land ((r \land \neg q \land \neg p) \lor(r \land \neg q \land \neg p)) \overset<\Leftrightarrow>$

$(p\lor q \lor r) \land r \land \neg q \land \neg p \overset<\Leftrightarrow>$

$r \land \neg q \land \neg p$

OK, so your clauses are: $\< r \>$ , $\< \neg q \>$ , and $\< \neg p\>$ . which can obviously be satisfied by setting $r$ to true, and $p$ and $q$ to false; exactly the assignment Andreas found as well.