Propositional logic · Free · No sign-up
Conjunctive Normal Form (CNF) Converter online
Type a formula, hit Convert to CNF and get its conjunctive normal form step by step: removing connectives, De Morgan's laws, double negation, the distributive property and simplification.
Convert formula to CNF
Use the buttons if you can't type the symbolsWhat is conjunctive normal form?
Conjunctive normal form (CNF) is a standard way of writing a propositional logic formula. A formula is in CNF when it is a conjunction of clauses, and each clause is a disjunction of literals. A literal is a variable (P) or its negation (¬P).
In other words, CNF is basically one big "AND" (∧) of several blocks, and inside each block there are only "OR" (∨) and negations attached to the letters. For example, (P ∨ ¬Q) ∧ (R ∨ Q ∨ ¬S) is in conjunctive normal form.
How to convert a formula to CNF in 5 steps
Every propositional formula has an equivalent in conjunctive normal form. The classic method has four steps plus an optional simplification step. The converter applies all of them, but it does the simplification inside step 4, on the fly (we explain this in step 5).
Step 1 · Remove every connective other than ∧ and ∨
We replace the connectives of the original formula with disjunctions (∨) and conjunctions (∧), based on the equivalences in the table:
| Formula | Equivalent |
|---|---|
| A → B | ¬A ∨ B |
| A ↔ B | (¬A ∨ B) ∧ (A ∨ ¬B) |
| A ⊕ B | (A ∧ ¬B) ∨ (¬A ∧ B) |
| A | B (NAND) | ¬(A ∧ B) |
| A ↓ B (NOR) | ¬(A ∨ B) |
Step 2 · Push negations down to the atoms (De Morgan's laws)
If after the previous step there is still a negation (¬) in front of a parenthesis, we "push it inside" using De Morgan's laws, until every negation affects only a single loose variable:
| Formula | Equivalent |
|---|---|
| ¬(A ∧ B) | ¬A ∨ ¬B |
| ¬(A ∨ B) | ¬A ∧ ¬B |
Step 3 · Remove double negations
Whenever a double negation appears we simplify it with ¬¬A ≡ A. When steps 2 and 3 are done, the formula only has ∧, ∨ and negations attached to the variables; that intermediate form is called negation normal form (NNF), and it is the starting point of the last step.
Step 4 · Apply the distributive property
Finally we distribute disjunction over conjunction as many times as needed, until the conjunctions are on the outside and the disjunctions on the inside:
| Formula | Equivalent |
|---|---|
| A ∨ (B ∧ C) | (A ∨ B) ∧ (A ∨ C) |
| (A ∧ B) ∨ C | (A ∨ C) ∧ (B ∨ C) |
Step 5 (optional) · Simplify, at the end or on the fly
This step is optional: once step 4 is done the formula is already in CNF, and simplifying does not change its logical meaning, it only makes it shorter. Even so, it is highly recommended, because the result is cleaner and it is usually required in class. You can do it just once at the end, when you already have the CNF, or at every iteration: before distributing and after each distribution. Both ways lead to an equivalent CNF, but the second one saves a lot of work: if something like q ∨ ¬q shows up, you replace it with 1 right then and don't drag it through all the following distributions. The converter simplifies at every iteration, so you won't see a separate step 5 in the result: each simplification appears as one more line of step 4, with the name of the law applied. If there is still something to remove at the end, a "Final cleanup" block is shown.
The laws used are complement (A ∨ ¬A ≡ 1, A ∧ ¬A ≡ 0), domination (A ∨ 1 ≡ 1, A ∧ 0 ≡ 0), identity (A ∨ 0 ≡ A, A ∧ 1 ≡ A), idempotence (A ∨ A ≡ A) and absorption (A ∨ (A ∧ B) ≡ A). If you only simplify at the end, on the finished CNF, they translate into these cases:
| Situation | What to do |
|---|---|
| Repeated clauses, for example: (q ∨ s ∨ ¬r) ∧ (s ∨ ¬r ∨ q) ∧ (s ∨ ¬r) | Keep only one of the two: (q ∨ s ∨ ¬r) ∧ (s ∨ ¬r) |
| A clause contains a variable both negated and not negated, for example: (¬q ∨ q ∨ ¬r ∨ s) | That clause is always true (tautology): it is removed entirely |
| Repeated literals within a clause, for example: (p ∨ p ∨ q) | Keep just one: (p ∨ q) |
| One clause contains another, for example: (s ∨ ¬r) ∧ (q ∨ s ∨ ¬r) | Absorption: the longer one is redundant, leaving (s ∨ ¬r) |
For example, the formula:
(¬q ∨ q ∨ ¬r ∨ s) ∧ (q ∨ s ∨ ¬r) ∧ (s ∨ ¬r ∨ q) ∧ (s ∨ q)
simplifies by removing the first clause (it is a tautology because it contains q and ¬q) and one of the two identical clauses, leaving simply:
(q ∨ s ∨ ¬r) ∧ (s ∨ q)
Worked example, step by step
Let's convert the formula (P ∨ ¬Q) ↔ R to CNF. This example uses all four steps.
- Step 1 — Remove the biconditional. With
A ↔ B ≡ (¬A ∨ B) ∧ (¬B ∨ A)(that is,(A→B) ∧ (B→A)), takingA = (P ∨ ¬Q)andB = R:
(¬(P ∨ ¬Q) ∨ R) ∧ (¬R ∨ (P ∨ ¬Q)) - Step 2 — De Morgan's laws. We push the negation of
¬(P ∨ ¬Q)with¬(A ∨ B) ≡ ¬A ∧ ¬B, keeping the parentheses that group that block:
((¬P ∧ ¬¬Q) ∨ R) ∧ (¬R ∨ (P ∨ ¬Q)) - Step 3 — Double negation.
¬¬Q ≡ Q, so the formula becomes:
((¬P ∧ Q) ∨ R) ∧ (¬R ∨ (P ∨ ¬Q)) - Step 4 — Distributive property. In the first block,
(¬P ∧ Q) ∨ R ≡ (¬P ∨ R) ∧ (Q ∨ R); the second block is already a disjunction:
(¬P ∨ R) ∧ (Q ∨ R) ∧ (¬R ∨ (P ∨ ¬Q))
and flattening the nested∨by associativity:
(¬P ∨ R) ∧ (Q ∨ R) ∧ (¬R ∨ P ∨ ¬Q)
Result (CNF): (¬P ∨ R) ∧ (Q ∨ R) ∧ (P ∨ ¬Q ∨ ¬R). In this case there is nothing to simplify, since no clause is a tautology or repeated, so we skip step 5. You can check this example by typing it into the converter.
Related calculators
All logic calculators (index)
Page with every tool related to this topic.
Disjunctive Normal Form (DNF) converter
The inverse method, step by step.
Truth Table Generator
For any propositional formula.
Rules of Inference Calculator
Prove an argument step by step with modus ponens, modus tollens and syllogisms.
Frequently asked questions
What is conjunctive normal form (CNF) used for?
CNF is used mainly for clause resolution (Robinson's method), where each disjunction becomes a clause, allowing you to check satisfiability, validity or unsatisfiability by refutation. It is also an intermediate step in Skolemization (via prenex CNF) and shows up in areas such as digital circuit design.
What is the difference between CNF and DNF?
In CNF the outer operator is conjunction (∧ of ∨). In disjunctive normal form (DNF) it is the other way around: a disjunction of conjunctions (∨ of ∧).
Can I use more than four variables?
Yes. The buttons show P, Q, R, S and T, but you can type any letter (A, B, C, x, y, z…) or names like p1, p2 directly in the field.