The clausal normal form (or clause normal form, conjunctive normal form, CNF) of a logical formula is used in logic programming

Logic programming

Logic programming is, in its broadest sense, the use of mathematical logic for computer programming. In this view of logic programming, which can be traced at least as far back as John McCarthy's [1958] advice-taker proposal, logic is used as a purely declarative representation language, and a...

 and many theorem proving

Automated theorem proving

Automated theorem proving or automated deduction, currently the most well-developed subfield of automated reasoning , is the proving of mathematical theorems by a computer program.- Decidability of the problem :...

 systems. A formula in clause normal form is a set of clauses, interpreted as a conjunction. A clause

Clause (logic)

In logic, a clause is a finite disjunction ofliterals. Clausesare usually written as follows, where the symbols l_i areliterals:l_1 \vee \cdots \vee l_nIn some cases, clauses are written as sets of literals, so that clause above...

 is an implicitly universally quantified set of literals, interpreted as a disjunction.

Conversion to clausal normal form

The procedure to convert a formula into clausal form can destroy the structure of the formula, and naive translations often causes exponential blowup

Exponential growth

Exponential growth occurs when the growth rate of a mathematical function is proportional to the function's current value...

 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. Standardize variables
   • becomes , where is new
3. Skolemize
   Skolem normal form
   Reduction to Skolem normal form is a method for removing existential quantifiers from formal logic statements, often performed as the first step in an automated theorem prover....
   
    -- replace existential
   Existential quantification
   In predicate logic, an existential quantification is the predication of a property or relation to at least one member of the domain. It is denoted by the logical operator symbol ∃ , which is called the existential quantifier...
   
    variables with Skolem constants or Skolem functions of universal
   Universal quantification
   In predicate logic, universal quantification formalizes the notion that something is true for everything, or every relevant thing....
   
    variables, from the outside inward. Make the following replacements:
   • becomes , where is new
4. Discard the universal quantifiers (which are implicit in CNF).
5. Put the formula into conjunctive normal form
   Conjunctive normal form
   In Boolean logic, a formula is in conjunctive normal form if it is a conjunction of clauses, where a clause is a disjunction of literals.As a normal form, it is useful in automated theorem proving...
   
   .
6. Replace with . Each conjunct is of the form , which is equivalent to .
7. Finally, replace each conjunct with .

When n ≤ 1 for all clauses, the logic is called Horn clause

Horn clause

In mathematical logic, a Horn clause is a clause with at most one positive literal. They are named after the logician Alfred Horn, who first pointed out the significance of such clauses in 1951...

 logic and is equivalent in computational power to a universal Turing machine

Universal Turing machine

In computer science, a universal Turing machine is a Turing machine that can simulate an arbitrary Turing machine on arbitrary input. The universal machine essentially achieves this by reading both the description of the machine to be simulated as well as the input thereof from its own tape. Alan...

. Horn logic is the basis of Prolog

Prolog

Prolog is a general purpose logic programming language associated with artificial intelligence and computational linguistics.Prolog has its roots in first-order logic, a formal logic, and unlike many other programming languages, Prolog is declarative: the program logic is expressed in terms of...

, the most widely used logic programming

Logic programming

Logic programming is, in its broadest sense, the use of mathematical logic for computer programming. In this view of logic programming, which can be traced at least as far back as John McCarthy's [1958] advice-taker proposal, logic is used as a purely declarative representation language, and a...

language.

Often it is sufficient to generate an equisatisfiable (not an equivalent) CNF for a formula. In this case, the worst-case exponential blow-up can be avoided by introducing definitions and using them to rename parts of the formula.