Converting to Clausal Form

Converting a propositional formula $\phi$ to sets of clauses can be accomplished, in general, in eight steps; they can be roughly summarized in sequence as follows.

1.

Eliminate all occurrences of $\rightarrow$ and $\leftrightarrow$, using two key facts, namely,

• $\phi \rightarrow \psi$ is equivalent to $\neg\phi \vee \psi$
• $\phi \leftrightarrow \psi$ is equivalent $(\phi \rightarrow \psi) \wedge (\psi \rightarrow \phi).$

2.

Distribute negations over other logical operators until they each apply to a single atomic formula, using three key facts, namely,

• $\neg \neg \phi$ is equivalent to $\phi$
• $\neg (\phi \wedge \psi)$ is equivalent to $\neg \phi \vee \neg \psi$
• $\neg (\phi \vee \psi)$ is equivalent to $\neg \phi \wedge \neg \psi$

3.

Convert to conjunctive normal form using the following rule:

• $\phi \vee (\psi \wedge \chi)$ can be replaced by $(\phi \vee \psi) \wedge (\phi \vee \chi)$

4.

Write conjunction from previous steps as set of clauses.

Here is a conversion of $(P \rightarrow Q) \wedge \neg P$:

step 1

$(\neg P \vee Q) \wedge P$

step 4

$\{\neg P, Q\} \hspace{.25in} \{P\}$

Here is a conversion of $(P \rightarrow Q) \wedge \neg Q$:

step 1

$(\neg P \vee Q) \wedge \neg Q$

step 4

$\{\neg P, Q\} \hspace{.1in} \{\neg Q\}$

Here is a slightly more involved conversion:

input

$(P \leftrightarrow Q) \wedge \neg Q$

step 1

$( (P \rightarrow Q) \wedge (Q \rightarrow P) ) \wedge \neg Q$

step 1

$( (\neg P \vee Q) \wedge (\neg Q \vee P) ) \wedge \neg Q$

step 4

$\{\neg P, Q\} \hspace{.1in} \{\neg Q, P\} \hspace{.1in} \{\neg Q\}$

Here is a conversion that uses steps 1, 2, and 4:

input

$\neg [((P \rightarrow Q) \wedge \neg Q) \rightarrow \neg P]$

step 1

$\neg [(((P \rightarrow Q) \wedge (Q \rightarrow P)) \wedge \neg Q) \rightarrow \neg P]$

step 1

$\neg [(((\neg P \vee Q) \wedge (\neg Q \vee P)) \wedge \neg Q) \rightarrow \neg P]$

step 1

$\neg [ \neg(((\neg P \vee Q) \wedge (\neg Q \vee P)) \wedge \neg Q) \vee \neg P]$

step 2

$\neg \neg (((\neg P \vee Q) \wedge (\neg Q \vee P)) \wedge \neg Q) \wedge \neg \neg P$

step 2

$(((\neg P \vee Q) \wedge (\neg Q \vee P)) \wedge \neg Q) \wedge P$

step 4

$\{\neg P, Q\} \hspace{.1in} \{\neg Q, P\} \hspace{.1in} \{\neg Q\} \hspace{.1in} \{P\}$

Here is a final example, one that uses all the four steps:

input

$P \vee ((Q \vee \neg Q) \rightarrow \neg P)$

step 1

$P \vee (\neg (Q \vee \neg Q) \vee \neg P)$

step 2

$P \vee ((\neg Q \wedge \neg \neg Q) \vee \neg P)$

step 3

$P \vee ((\neg P \vee \neg Q) \wedge (\neg P \vee Q))$

step 3

$(P \vee (\neg P \vee \neg Q)) \wedge (P \vee (\neg P \vee Q))$

step 4

$\{P, \neg P, \neg Q\} \hspace{.1in} \{P, \neg P, Q\}$