Conversion from PL to CNF

Question

I am trying to convert some formulas into CNF even if I understood both concepts and rules of it I cannot always get a solution. For example I have this statement to convert: $(p\Leftrightarrow p)\Rightarrow (\neg p \wedge r)$. Applying the rules I get this formula (that I know it is right since the solution for both formulas is the same according to Wolfram) $(p \wedge \neg q) \vee (q \wedge \neg p) \vee (\neg p \wedge r)$. From this position I know I should apply some distributive law to "move the OR inside and the AND outside" but I really don't get how. I already know the result that is $(\neg p \vee \neg q) \wedge (p \vee q \vee r)$.

Answer 1

There are several options how you could apply distributive law. Here's one. The version I'm using says that $(A \land B) \lor C \equiv (A \lor C) \land (B \lor C)$. Let's apply this to your formula $$(p \land \lnot q) \lor (q \land \lnot p) \lor (\lnot p \land r)$$ Here you can set $A := p$, $B := \lnot q$ and $C := (q \land \lnot p) \lor (\lnot p \land r)$. Then distributivity yields $$(p \lor (q \land \lnot p) \lor (\lnot p \land r)) \land (\lnot q \lor (q \land \lnot p) \lor (\lnot p \land r))$$

We need to apply distributivity a few times more. Consider the left side first. $$(p \lor (q \land \lnot p) \lor (\lnot p \land r)) \equiv [(p \lor q) \land (p \lor \lnot p)] \lor (\lnot p \land r) \equiv (p \lor q) \lor (\lnot p \land r) \\ \equiv (p \lor q \lor \lnot p) \land (p \lor q \lor r) \equiv p \vee q \vee r$$

Here I used the law that $A \wedge \top \equiv A$ twice, removing the tautologous $(p \vee \lnot p)$ and $(p \vee q \vee \lnot p)$.

Let's turn to the right-hand side. By similar reductions as in the first step, you get $$(\lnot q \lor (q \land \lnot p) \lor (\lnot p \land r)) \equiv (\lnot q \lor \lnot p \lor \lnot p) \wedge (\lnot q \lor \lnot p \lor r)$$

By the law that $(A \lor B) \wedge (A \lor B \lor C) \equiv A \lor B$, this is equivalent to $$\lnot q \lor \lnot p$$

Thus, combining the results we get $(p \vee q \vee r) \wedge (\lnot q \lor \lnot p)$, as desired.