CIS 554: Conversion to Clause Form

Fall 2010, David Matuszek

- Eliminate logical implications,
`⇒`

, using the fact that`A ⇒ B`

is equivalent to`¬A ∨ B`

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

- Standardize variables so that each quantifier binds a unique variable.
- Move all quantifiers to the left, maintaining their order.
- 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)`

- Drop the prefix; assume universal quantification.

Note: The term prefix refers to all the quantifiers; the matrix is everything else. - Convert the matrix into a conjunction of disjuncts.
- Create a separate clause corresponding to each conjunct.
- Standardize apart the variables in the clauses.