Clausal Normal Form - Conversion To Clausal Normal Form

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 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 -- replace existential variables with Skolem constants or Skolem functions of universal 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.
  6. Replace with . Each conjunct is of the form, which is equivalent to .

When n ≤ 1 for all clauses, the logic is called Horn clause logic and is equivalent in computational power to a universal Turing machine. Horn logic is the basis of Prolog, the most widely used logic programming 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.

Read more about this topic:  Clausal Normal Form

Famous quotes containing the words conversion, normal and/or form:

    “The conversion of a savage to Christianity is the conversion of Christianity to savagery.”
    —George Bernard Shaw (1856–1950)

    “Like sleep disturbances, some worries at separation can be expected in the second year. If you accept this, then you will avoid reacting to this anxiety as if it’s your fault. A mother who feels guilty will appear anxious to the child, as if to affirm the child’s anxiety. By contrast, a parent who understands that separation anxiety is normal is more likely to react in a way that soothes and reassures the child.”
    —Cathy Rindner Tempelsman (20th century)

    “Women stand related to beautiful nature around us, and the enamoured youth mixes their form with moon and stars, with woods and waters, and the pomp of summer. They heal us of awkwardness by their words and looks. We observe their intellectual influence on the most serious student. They refine and clear his mind: teach him to put a pleasing method into what is dry and difficult.”
    —Ralph Waldo Emerson (1803–1882)