Convert a logical expression to conjunctive normal form

Question

Goal:

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.

Input:

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.

Output:

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)))

Notes:

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 code-golf; shortest answer (in bytes) wins.

Answer 1

You're going to hate me....

Mathematica, 23 bytes

#~BooleanConvert~"CNF"&

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

TraditionalForm[#~BooleanConvert~"CNF"]&

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

Answer 2

Maxima, 4 bytes

pcnf

Try It Online!

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

Answer 3

JavaScript (ES6), 127 bytes

f=(s,t='',p=s.match(/[A-Z]/),r=RegExp(p,'g'))=>p?'('+f(s.replace(r,1),t+'|'+p)+')&('+f(s.replace(r,0),t+'|!'+p)+')':eval(s)?1:0+t

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

• (: (
• ): )
• ⊤: 1
• ⊥: 0
• ¬: !
• ⇒: <=
• ⇔: ==
• ∧: &
• ∨: |

Examples:

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:

f=(s,t='',p=s.match(/[A-Z]/),r=RegExp(p,'g'))=>p?'('f(s.replace(r,1),t+'&'+p)+')|('+f(s.replace(r,0),t+'&!'+p)+')':eval(s)?1+t:0

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)))