CIS 554: Conversion to Clause Form
Fall 2010, David Matuszek

These rules are adapted from Artificial Intelligence, by Elaine Rich and Kevin Knight.
1. Eliminate logical implications,` ⇒`, using the fact that` A ⇒ B `is equivalent to` ¬A ∨ B`.
2. Reduce the scope of each negation to a single term, using the following facts:
```      ¬(¬P) = P
¬(A ∨ B) = ¬A ∧ ¬B
¬(A ∧ B) = ¬A V ¬B
¬∀x: P(x) = ∃x: ¬P(x)
¬∃x: P(x) = ∀x: ¬P(x)```
3. Standardize variables so that each quantifier binds a unique variable.
4. Move all quantifiers to the left, maintaining their order.
5. Eliminate existential quantifiers, using Skolem functions (functions of the preceding universally quantified variables). Examples:
`∃x: P(x) becomes x'`
`∀x: ∃y: P(y) becomes ∀x: y'(x)`
6. Drop the prefix; assume universal quantification.
Note: The term prefix refers to all the quantifiers; the matrix is everything else.
7. Convert the matrix into a conjunction of disjuncts.
8. Create a separate clause corresponding to each conjunct.
9. Standardize apart the variables in the clauses.