The Artima Developer Community
Sponsored Link

CNF Converter

Advertisement

This page will convert your propositional logic formula to conjunctive normal form. Just type it in below and press the "Convert" button:

Your Formula:

A propositional logic formula is a combination of atomic formulas (or simply, atoms) and logical connectives. An atom is a logical proposition that doesn't contain any logical connectives, such as, Q or Glorp. Each atom can be interpreted as standing for some statement in human language that can be either true or false. For example, Q could stand for the statement "The cat is under the bed." The logical connectives are: AND, OR, NOT, CONDITIONAL, and BICONDITIONAL. (CONDITIONAL means if-then; BICONDITONAL means if-and-only-if.)

The formula you enter above must use the following symbols for logical connectives:

AND:&
OR:|
NOT:~
CONDITIONAL:=> or <=
BICONDITIONAL:<=>

Atoms must start with a letter and can subsequently contain numbers and the symbols {, }, -, and +. Some valid atoms: "A", "ThisIsReallyGroovy", "X{k-1}", "Y{k+1}", "bob".

The CNF Converter is uptight about parentheses. You must place parentheses around terms joined by an AND, OR, CONDITIONAL, or BICONDITIONAL. So "(A & ~B)" is OK, where "A & ~B" is not. But you can't place parentheses around atoms and negations. So "A" and "~A" are OK, but "(A)" and "(~A)" are not.

Some valid propositional logic formulas:

   (~A & B)
   ~((A | ~B)<=>C)
   (X{k} <=> (Y{k} & (Z{k} | X{k-1})))
   (cat => mouse)
   (cat <= dog)

A propositional logic formula is in conjunctive normal form if it is a conjunction of clauses where each clause is a disjunction of atoms. A conjunction is a set of formulas connected by AND, and a disjunction is a set of formulas connected by OR.

The CNF Converter will use the following algorithm to convert your formula to conjunctive normal form:

Implications out:

    A => B    --->    ~A | B
    A <= B    --->    A | ~B
    A <=> B   --->    (~A | B) & (A | ~B)

Negations in:

    ~~p         --->    p
    ~(A & B)  --->    ~A | ~B
    ~(A | B)  --->    ~A & ~B

Disjunctions in:

    A | (B & C)  --->  (A | B) & (A | C)

Sponsored Links



Google
  Web Artima.com   
Copyright © 1996-2019 Artima, Inc. All Rights Reserved. - Privacy Policy - Terms of Use