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.