Converting to Clausal Form

Converting a closed formula of $\cal L$_I to clausal form can be accomplished by following the steps given in Chapter 2, along with new steps that arise from the presence of quantifiers and variables. (In Chapter 2, recall, we dealt only with the propositional case.) The procedure is composed of 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 five 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$
• $\neg \forall x \phi$ becomes $\exists x \neg \phi$
• $\neg \exists x \phi$ becomes $\forall x \neg \phi$

3.

Rename variables, giving each quantifier a unique variable;

4.

Eliminate all existential quantifiers (this involves skolemizing, which is explained below);

5.

Drop all universal quantifiers;

6.

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)$

7.

Write conjunction from previous steps as set of clauses;

8.

Rename variables so that no variable appears in more than one class.