I tried to convert this to a CNF-expression but failed.

What did I do wrong? Or are there simply missing steps?

$$ F' = (( A \lor \lnot B) \land C) \to ( \lnot A \land C) $$ Removed Implication $$ \equiv \lnot(( A \lor \lnot B) \land C) \lor ( \lnot A \land C) $$ de Morgan $$ \equiv ( \lnot ( A \lor \lnot B) \lor \lnot C) \lor ( \lnot A \land C) $$ de Morgan $$ \equiv (( \lnot A \land \lnot \lnot B) \lor \lnot C) \lor ( \lnot A \land C) $$ double Negation $$ \equiv (( \lnot A \land B) \lor \lnot C) \lor ( \lnot A \land C) $$ distributive law $$ \equiv (( \lnot C \lor \lnot A) \land (\lnot C \lor B)) \lor (\lnot A \land C) $$ distributive law $$ \equiv ((\lnot A \land C) \lor (\lnot C \lor \lnot A)) \land ((\lnot A \land C) \lor (\lnot C \lor B)) $$


Your application of double negation elimination got you a statement in negation normal form, which is the first step in conversion to CNF.

$$F' \equiv ((\neg A \wedge B) \vee \neg C) \vee (\neg A \wedge C)$$


$$\equiv ((\neg A \vee \neg C) \wedge (B \vee \neg C)) \vee (\neg A \wedge C)$$


$$\equiv ((\neg A \vee \neg C) \vee (\neg A \wedge C)) \wedge ((B \vee \neg C) \vee (\neg A \wedge C))$$


$$\equiv ((\neg A \vee (\neg A \vee \neg C)) \wedge (C \vee (\neg A \vee \neg C))) \wedge ((B \vee \neg C) \vee (\neg A \wedge C))$$

Now we omit some brackets for clarity:

$$\equiv (\neg A \vee \neg A \vee \neg C) \wedge (C \vee \neg A \vee \neg C) \wedge ((B \vee \neg C) \vee (\neg A \wedge C))$$

Apply distributivity on the right again:

$$\equiv (\neg A \vee \neg A \vee \neg C) \wedge (C \vee \neg A \vee \neg C) \wedge ((\neg A \vee (B \vee \neg C)) \wedge (C \vee (B \vee \neg C)))$$

Take out some more brackets:

$$\equiv (\neg A \vee \neg A \vee \neg C) \wedge (C \vee \neg A \vee \neg C) \wedge (\neg A \vee B \vee \neg C) \wedge (C \vee B \vee \neg C)$$

Now we remove tautologous clauses and duplicated literals:

$$\equiv (\neg A \vee \neg C) \wedge (\neg A \vee B \vee \neg C)$$

And there we go: an expression in conjunctive normal form equivalent to the initial one. It's worth checking their respective truth tables, of course, to make sure.


Everything so far is all right, but you aren't finished. CNF means that the formula has the form $C_1\land C_2\land\cdots\land C_n$, where each of the $C_i$ has the form $L_1\lor L_2\lor\cdots\lor L_n$, where each $L_i$ is a literal or a negation of a literal. For example:

$$ (A\lor\lnot B)\land (\lnot A\lor B \lor C) \land (B\lor C\lor \lnot D)$$

Your last line has the form $X_1 \land X_2$, but neither the left nor the right conjunct is in the simple form that is required for CNF. The conjuncts should contain nothing but disjunctions of literals and negated literals.

You might want to review the Wikipedia article about it, which has more examples.

  • $\begingroup$ Is it safe to remove the braces around the double negation removal? My prof always uses soooo many braces, that I don't know when I am allowed to remove them ^^' $\endgroup$ – Sven Feb 20 '13 at 16:56
  • $\begingroup$ I don't see any braces that you removed after the double-negation removal. The lines before and after that step each have three pairs of braces. $\endgroup$ – MJD Feb 20 '13 at 17:16
  • $\begingroup$ I mean ((¬A∧B)∨¬C)∨(¬A∧C) --> (¬A∧B)∨¬C∨(¬A∧C) $\endgroup$ – Sven Feb 20 '13 at 17:21
  • $\begingroup$ You could do that, but if the brackets worry you, I suggest that you leave them in, and always have one pair of brackets for each $\lor$ or $\land$ in a formula. $\endgroup$ – MJD Feb 20 '13 at 18:41

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.