CSE 463/563, Spring 2005

Clause Form

Last Update: 14 February 2005

Note: or material is highlighted

Notation: $X \rightarrow Y$ for: Rewrite all occurrences of $X$ as $Y$.

Algorithm Clause-Form;

Input A wff $\alpha$ of FOL (or propositional logic);
Output A logically equivalent formula in clause form;

begin

1. Convert $\alpha$ to a logically equivalent formula in Prenex Normal Form:
   1. $(\alpha \equiv \beta) \rightarrow ((\alpha \supset \beta) \wedge (\beta \supset \alpha))$
   2. $(\alpha \supset \beta) \rightarrow (\neg\alpha \vee \beta)$
   3. repeat:
      1. $\neg\neg\alpha \rightarrow \alpha$
      2. $\neg(\alpha \wedge \beta) \rightarrow (\neg \alpha \vee \neg\beta)$
      3. $\neg(\alpha \vee \beta) \rightarrow (\neg \alpha \wedge \neg\beta)$
      4. $\neg\exists x [\alpha] \rightarrow \forall x[\neg \alpha]$
      5. $\neg\forall x[\alpha] \rightarrow \exists x[\neg \alpha]$
      until "$\neg$" only applies to atomic wffs;
   4. begin optional section:
      1. $(\alpha \vee \alpha ) \rightarrow \alpha$
      2. $(\alpha \wedge \alpha ) \rightarrow \alpha$
      end optional section;
   5. Rename variables such that variables bound by different quantifiers have unique names
   6. Move all quantifiers to the left, without changing their order
2. Convert PNF($\alpha$) to Skolem Normal Form:
   repeat:
   1. $\forall x_1 \ldots \forall x_n \exists y [\alpha (y)] \rightarrow \forall x_1 \ldots \forall x_n [\alpha (f(x_1 \ldots x_n))]$ // $f$ is a new Skolem function
   2. $\exists y [\alpha (y)] \rightarrow \alpha (c)$ // $c$ is a new Skolem constant
   until all existential quantifiers are eliminated

3. Convert SNF($\alpha$) to Conjunctive Normal Form:
   1. $\forall x [\alpha (x)] \rightarrow \alpha (x)$
   2. repeat:
      1. $(\alpha \vee ( \beta \wedge \gamma )) \rightarrow ((\alpha \vee \beta ) \wedge (\alpha \vee \gamma ))$
      2. begin optional section:
         1. $(\alpha \vee \alpha ) \rightarrow \alpha$
         2. $(\alpha \wedge \alpha ) \rightarrow \alpha$
         end optional section;

      until the formula is a conjunction of disjunctions of literals

4. (optionally:) Convert CNF($\alpha$) to Clause Form:
   1. $(\alpha \vee \beta ) \rightarrow \alpha\beta$ (or: $[\alpha , \beta ]$) // $\alpha\beta$ (or: $[\alpha , \beta ]$) is a "clause"
   2. $(\alpha \wedge \beta ) \rightarrow \{\alpha , \beta \}$ // these are sets of clauses
   3. Rename variables again such that each clause has different variables

end.