Clausal normal form

The clausal normal form is used in logic programming and many theorem proving systems. The procedure to put a formula into clausal form destroys the structure of the formula and often causes exponential blowup in the size of the resulting formula.

The procedure begins with any formula of classical first-order logic:

1. Put the formula into negation normal form.
2. Skolemize -- replace existential variables with Skolem constants or Skolem functions of universal variables, from the outside inward. Make the following replacements:
   • Exists x. P(x) becomes P(c), where c is new
   • Forall x. ... Exists y. P(y) becomes Forall x. ... P(f_c(x)), where f_c is new
3. Remove the quantifiers.
4. Put the formula into conjunctive normal form.
5. Replace with {C1,...,Cn}. Each conjunct is of the form , which is equivalent to .
   • If m=0 and n=1, this is a Prolog fact.
   • If m>0 and n=1, this is a Prolog rule.
   • If m>0 and n=0, this is a Prolog query.
6. Finally, replace each conjunct with .

When n=1, the logic is called Horn clause logic and is equivalent in computational power to a universal Turing machine.