How to use resolution to prove a sentence is unsatisfiable?

Question

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\}}$ $\{r, \neg q, \neg p\}$. With resolution, I know that if you have something like $\{p, \neg q\}$ and $\{q, \neg p\}$ then the negations would cancel out but you can only do one at a time so you'd get both $\{p, \neg p \}$ and $\{q, \neg q\}$. 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 $\{p, q, \neg p, \neg q\}$? 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?

Answer 1

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{Implication, Reduction}{\Leftrightarrow}$

$(p\lor q \lor r) \land (\neg (\neg r \lor q \lor p) \lor(r \land \neg q \land \neg p)) \overset{DeMorgan}{\Leftrightarrow}$

$(p\lor q \lor r) \land ((r \land \neg q \land \neg p) \lor(r \land \neg q \land \neg p)) \overset{Idempotence}{\Leftrightarrow}$

$(p\lor q \lor r) \land r \land \neg q \land \neg p \overset{Absorption}{\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.

Answer 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 $\{\{p, q , r\}, \{r\},\{\lnot q\},\{\lnot p\}\}$ which almost immediately resolves down to $\{\{r\},\{\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 $\{\{p, q , \lnot r\}, \{r\},\{\lnot q\},\{\lnot p\}\}$ .