Write a complete program or function which takes a formula in propositional logic (henceforth referred to as a logical expression or expression) and outputs that formula in conjunctive normal form. There are two constants, and representing true and false, a unary operator ¬ representing negation, and binary operators , , , and representing implication, equivalence, conjunction, and disjunction, respectively which obey all of the usual logical operations (DeMorgan's law, double negation elimination, etc.).

Conjunctive normal form is defined as follows:

  1. Any atomic expression (including and ) is in conjunctive normal form.
  2. The negation of any previously constructed expression is in conjunctive normal form.
  3. The disjunction of any two previously constructed expressions is in conjunctive normal form.
  4. The conjunction of any two previously constructed expressions is in conjunctive normal form.
  5. Any other expression is not in conjunctive normal form.

Any logical expression can be converted (non-uniquely) into a logically equivalent expression in conjunctive normal form (see this algorithm). You do not need to use that particular algorithm.


You may take input in any convenient format; e.g., a symbolic logical expression (if your language supports it), a string, some other data structure. You do not need to use the same symbols for true, false, and the logical operators as I do here, but your choice should be consistent and you should explain your choices in your answer if it's not clear. You may not accept any other input or encode any additional information in your input format. You should have some way of expressing an arbitrary number of atomic expressions; e.g. integers, characters, strings, etc.


The formula in conjunctive normal form, again in any convenient format. It need not be in the same format as your input, but you should explain if there are any differences.

Test cases:

P ∧ (P ⇒ R) -> P ∧ R
P ⇔ (¬ P) -> ⊥
(¬ P) ∨ (Q ⇔ (P ∧ R)) -> ((¬ P) ∨ ((¬ Q) ∨ R)) ∧ ((¬ P) ∨ (Q ∨ (¬ R)))


  1. If the input expression is a tautology, would be a valid output. Similarly, if the input expression is a contradiction, would be a valid output.
  2. Both your input and output formats should have a well-defined order of operations capable of expressing all possible logical expressions. You may need parentheses of some sort.
  3. You may use any well-defined choice of infix, prefix, or postfix notation for the logical operations. If your choice differs from the standard (negation is prefix, the rest are infix), please explain that in your answer.
  4. Conjunctive normal form is not unique in general (not even up to reordering). You need only to output a valid form.
  5. However you represent atomic expressions, they must be distinct from the logical constants, operators, and grouping symbols (if you have them).
  6. Built-ins which compute conjunctive normal form are allowed.
  7. Standard loopholes are forbidden.
  8. This is ; shortest answer (in bytes) wins.
  • \$\begingroup\$ related \$\endgroup\$
    – user61980
    Commented Jan 31, 2017 at 5:49
  • 1
    \$\begingroup\$ CNF isn't unique up to reordering: the equivalent expressions P and (P ∨ Q) ∧ (P ∨ (¬Q)) are both in conjunctive normal form. \$\endgroup\$ Commented Jan 31, 2017 at 6:03
  • 1
    \$\begingroup\$ Checking for tautology/contradiction is a second task unrelated to CNF transformation, so I would suggest to drop this requirement and put in into its own challenge. \$\endgroup\$
    – Laikoni
    Commented Jan 31, 2017 at 6:15
  • \$\begingroup\$ @Laikoni Very true. I updated the question to say that those are possible outputs for tautologies and contradictions rather than required outputs. \$\endgroup\$
    – user61980
    Commented Jan 31, 2017 at 6:19

3 Answers 3


You're going to hate me....

Mathematica, 23 bytes


The input will use True and False instead of and , but otherwise will look very similar to the notation of the question: all of the characters ¬, , , , and are recognized in Mathematica (when input with UTF-8 characters 00AC, F523, 29E6, 2227, and 2228, respectively), and parentheses act as you would expect.

By default, the output will use Mathematica's preferred symbols: for example, the last test case will output (! P || ! Q || R) && (! P || Q || ! R) instead of ((¬ P) ∨ ((¬ Q) ∨ R)) ∧ ((¬ P) ∨ (Q ∨ (¬ R))). However, changing the function to


will make the output look pretty and conforming to these usual symbols:

traditional form


Maxima, 4 bytes


Try It Online!

You can use implies, eq, and, or operators for implication, equivalence, conjunction, and disjunction respectively.

  • \$\begingroup\$ The online sample doesn't work anymore, but here's an example: First load(logic), then: pcnf((c and (a or b)) or (a and b)). The response is: (a or b or c) and (not a or b or c) and (not b or a or c) and (not c or a or b) \$\endgroup\$ Commented Jul 13, 2022 at 22:20

JavaScript (ES6), 127 bytes


I/O format is as follows (in order of precedence):

  • (: (
  • ): )
  • : 1
  • : 0
  • ¬: !
  • : <=
  • : ==
  • : &
  • : |


P&(P<=R) -> ((1)&(0|P|!R))&((0|!P|R)&(0|!P|!R))
P==(!P) -> (0|P)&(0|!P)
(!P)|(Q==(P&R)) -> (((1)&(0|P|Q|!R))&((0|P|!Q|R)&(1)))&(((1)&(1))&((1)&(1)))

The function is trivially rewritten to produce disjunctive normal form:


8 bytes could be saved from this version if I was allowed to assume the above precedence on output too, which would remove all the parentheses from the output examples:

P&(P<=R) -> ((1&P&R)|(0))|((0)|(0))
P==(!P) -> (0)|(0)
(!P)|(Q==(P&R)) -> (((1&P&Q&R)|(0))|((0)|(1&P&!Q&!R)))|(((1&!P&Q&R)|(1&!P&Q&!R))|((1&!P&!Q&R)|(1&!P&!Q&!R)))

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.