Propositional Logic · Free · No Sign Up

Conjunctive Normal Form (CNF) Converter

Q: What is Conjunctive Normal Form (CNF) used for?

Una fórmula escrita como conjunción (∧) de cláusulas, donde cada cláusula es una disyunción (∨) de literales. Una gran «Y» de varios «O». La FNC se usa principalmente para la resolución de cláusulas (método de Robinson), donde cada disyunción pasa a ser una cláusula, permitiendo comprobar satisfacibilidad, validez o insatisfacibilidad por refutación. También es un paso intermedio en la skolemización (vía FNC prenexa) y aparece en áreas como el diseño de circuitos digitales.

Enter a formula, click Calculate CNF, and get its conjunctive normal form step-by-step: connector elimination, De Morgan's laws, double negation, distributive property, and simplification.

CNF Converter

Click the buttons if you don't know how to type the symbols

Operators

Variables

Examples: (P → Q) ∧ (Q → R) (P ∨ ¬Q) ↔ R ¬(P ∧ (Q ∨ R)) (A ∨ B) ∧ (¬A → C)

What 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, where each clause is a disjunction of literals. A literal is either a variable (P) or its negation (¬P).

In other words, CNF is essentially a large "AND" (∧) of several blocks, and within each block, there are only "OR" (∨) operators and negations attached to the variables. 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 one optional), which are exactly the ones applied by the converter.

Step 1 · Eliminate connectors other than ∧ and ∨

We replace the connectors 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 inward to the atoms (De Morgan's Laws)

If after the previous step there is any negation (¬) in front of a parenthesis, we "push" it inside using De Morgan's laws, until each negation affects only a single variable:

Formula	Equivalent
¬(A ∧ B)	¬A ∨ ¬B
¬(A ∨ B)	¬A ∧ ¬B

Step 3 · Eliminate double negations

Whenever a double negation appears, we simplify it using ¬¬A ≡ A. After completing steps 2 and 3, the formula only contains ∧, ∨, and negations attached directly to the variables; this intermediate state is called negation normal form (NNF), and it is the starting point for the final step.

Step 4 · Apply the distributive property

Finally, we distribute the disjunction over the conjunction as many times as necessary, until the conjunctions are on the outside and the disjunctions are on the inside:

Formula	Equivalent
A ∨ (B ∧ C)	(A ∨ B) ∧ (A ∨ C)
(A ∧ B) ∨ C	(A ∨ C) ∧ (B ∨ C)

Step 5 (optional) · Simplify the resulting formula

Once in CNF, we can sometimes simplify the formula without altering its logical meaning. The standard simplifications are:

Situation	What to do
Repeated clauses, for example: (q ∨ s ∨ ¬r) ∧ (s ∨ ¬r ∨ q) ∧ (s ∨ ¬r)	Keep only one of them: (q ∨ s ∨ ¬r) ∧ (s ∨ ¬r)
A clause contains a variable and its negation, for example: (¬q ∨ q ∨ ¬r ∨ s)	That clause is always true (tautology): eliminate it completely
Repeated literals within a clause, for example: (p ∨ p ∨ q)	Keep only one: (p ∨ q)

For example, the formula:

(¬q ∨ q ∨ ¬r ∨ s) ∧ (q ∨ s ∨ ¬r) ∧ (s ∨ ¬r ∨ q) ∧ (s ∨ q)

is simplified by removing the first clause (it's a tautology because it contains q and ¬q) and one of the two identical clauses, leaving simply:

(q ∨ s ∨ ¬r) ∧ (s ∨ q)

Ejemplo resuelto paso a paso

Pasemos a FNC la fórmula (P ∨ ¬Q) ↔ R. Este ejemplo usa los cuatro pasos.

Paso 1 — Eliminar el bicondicional. Con A ↔ B ≡ (¬A ∨ B) ∧ (¬B ∨ A) (es decir, (A→B) ∧ (B→A)), tomando A = (P ∨ ¬Q) and B = R:
(¬(P ∨ ¬Q) ∨ R) ∧ (¬R ∨ (P ∨ ¬Q))
Paso 2 — Leyes de Morgan. Empujamos la negación de ¬(P ∨ ¬Q) con ¬(A ∨ B) ≡ ¬A ∧ ¬B, conservando los paréntesis que agrupan ese bloque:
((¬P ∧ ¬¬Q) ∨ R) ∧ (¬R ∨ (P ∨ ¬Q))
Paso 3 — Doble negación. ¬¬Q ≡ Q, de manera que la fórmula quedaría tal que así:
((¬P ∧ Q) ∨ R) ∧ (¬R ∨ (P ∨ ¬Q))
Paso 4 — Propiedad distributiva. En el primer bloque, (¬P ∧ Q) ∨ R ≡ (¬P ∨ R) ∧ (Q ∨ R); el segundo bloque ya es una disyunción:
(¬P ∨ R) ∧ (Q ∨ R) ∧ (¬R ∨ (P ∨ ¬Q))
y aplanando los ∨ anidados por asociatividad:
(¬P ∨ R) ∧ (Q ∨ R) ∧ (¬R ∨ P ∨ ¬Q)

Resultado (FNC): (¬P ∨ R) ∧ (Q ∨ R) ∧ (P ∨ ¬Q ∨ ¬R). En este caso no hay nada que simplificar, ya que ninguna cláusula es tautología ni se repite, y por tanto omitimos el paso 5. Puedes comprobar la solución de este ejemplo escribiéndolo en la calculadora.

Calculadoras relacionadas

∨∧

Disjunctive Normal Form (DNF)

The inverse method, step by step.

▦

Truth Tables

De cualquier fórmula proposicional. pronto

∴

Resolución / cláusulas

Refutación y cláusula vacía. pronto

Frequently Asked Questions (FAQs)

What is Conjunctive Normal Form (CNF) used for?

CNF is primarily used for clause resolution (Robinson's resolution method), where each disjunction becomes a clause, allowing for the verification of satisfiability, validity, or unsatisfiability through refutation. It is also an intermediate step in Skolemization (via prenex CNF) and is applied in areas such as digital circuit design.

What is the difference between CNF and DNF?

In CNF, the outermost operator is a conjunction (∧ of ∨). In Disjunctive Normal Form (DNF), it is the exact opposite: a disjunction of conjunctions (∨ of ∧).

Can I use more than four variables?

Yes. The buttons display P, Q, R, S, and T, but you can type any letter (A, B, C, x, y, z...) or names like p1, p2 directly into the input field.