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

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:

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)