Show with resolution proof that expression is a tautology

Question

I have the boolean expression:

$$ ((\neg A \lor B) \land (\neg B \lor \neg C))\implies (A\implies \neg C) $$

I have reshaped this so far that no equivalence and no implication is included. As far as I know, it is important for the resolution that the Boolean function is in CNF. My transformation then flows into this expression: $$ ((\neg A \lor B) \land (\neg B \lor \neg C))\implies (A\implies \neg C) $$ $$ ((\neg A \lor B) \land (\neg B \lor \neg C))\implies (\neg A \lor \neg C) $$ $$ \neg((\neg A \lor B) \land (\neg B \lor \neg C))\lor (\neg A \lor \neg C) $$ $$ (\neg(\neg A \lor B) \lor \neg(\neg B \lor \neg C))\lor (\neg A \lor \neg C) $$ $$ ((A \land \neg B) \lor (B \land C))\lor (\neg A \lor \neg C) $$ That is not yet CNF form, right? My question is therefore, can someone go to me the transformation steps? How to get to the CNF form?

If I had the CNF form, I could show a tautology with the resolution. For this I need the clause set from the CNF.

Answer 1

To get into CNF, distribute any $\lor$'s over $\land$'s. So:

$$ ((A \land \neg B) \lor (B \land C))\lor (\neg A \lor \neg C) \Leftrightarrow$$

$$ (((A \land \neg B) \lor B) \land (A \land \neg B) \lor C))) \lor (\neg A \lor \neg C) \Leftrightarrow$$

$$ ((A \lor B) \land (\neg B \lor B) \land (A \lor C) \land (\neg B \lor C)) \lor (\neg A \lor \neg C) \Leftrightarrow$$

$$ ((A \lor B) \land \top \land (A \lor C) \land (\neg B \lor C)) \lor (\neg A \lor \neg C) \Leftrightarrow$$

$$ ((A \lor B) \land (A \lor C) \land (\neg B \lor C)) \lor (\neg A \lor \neg C) \Leftrightarrow$$

$$ ((A \lor B) \lor (\neg A \lor \neg C)) \land ((A \lor C) \lor (\neg A \lor \neg C)) \land ((\neg B \lor C) \lor (\neg A \lor \neg C)) \Leftrightarrow$$

$$ (A \lor B \lor \neg A \lor \neg C) \land (A \lor C \lor \neg A \lor \neg C) \land (\neg B \lor C \lor \neg A \lor \neg C) \Leftrightarrow$$

$$ \top \land \top \land \top \Leftrightarrow$$

$$\top$$

Hmmm....

OK, so we have taken the statement as is and proven it to be a tautology!

... but not through resolution ...

In fact, you got the wrong set-up! To prove this statement to be a tautology through resolution, you need to first negate the statement, and then put it into CNF, thus into clauses, and then derive the empty clause through resolution:

$$ \neg (((\neg A \lor B) \land (\neg B \lor \neg C))\to (A\to \neg C)) \Leftrightarrow$$

$$ ((\neg A \lor B) \land (\neg B \lor \neg C))\land \neg (A \to \neg C) \Leftrightarrow$$

$$ (\neg A \lor B) \land (\neg B \lor \neg C)\land A \land C$$

This is now in CNF! ... and you will find resolution is now trivial

Answer 2

To prove $(X\wedge Y)\to Z$ is a tautology, by resolution, you seek to prove $(X\wedge Y\wedge\neg Z)$ is a contradiction (ie false).   After all, if the junction of $X$ and $Y$ does imply $Z$ then it shall contradict $\neg Z$.

So, since the negation of $A\to\neg C$ is $A\wedge\neg\neg C$, therefore to prove $((\neg A\vee B)\wedge(\neg B\vee\neg C))\to(A\to\neg C)$, you must simply show that $((\neg A\vee B)\wedge(\neg B\vee\neg C))\wedge(A\wedge\neg\neg C)$ is a contradiction.

That is, that the clausal form $\{(\neg A, B),(\neg B,\neg C),(A),(\neg\neg C)\}$ may be resolved to an empty set.