Home

Tseytin Transformation

Convert a propositional formula to equisatisfiable CNF — step by step

QF_PROP → CNF
Formula Input
Operators: ! not  |  & and  |  | or  |  -> implies  |  <-> iff  |  Atoms: uppercase letters, true, false
E(C) Transformation Rules
(¬pC ∨ C) ∧ (¬C ∨ pC)
C is variable
(¬pC ∨ ⊤) ∧ (⊥ ∨ pC)
C is true
(¬pC ∨ ⊥) ∧ (⊤ ∨ pC)
C is false
(¬pC ∨ ¬pD) ∧ (pD ∨ pC)
C = ¬D
(¬pC ∨ pC₁) ∧ (¬pC ∨ pC₂) ∧ (¬pC₁ ∨ ¬pC₂ ∨ pC)
C = C₁ ∧ C₂
(¬pC ∨ pC₁ ∨ pC₂) ∧ (¬pC₁ ∨ pC) ∧ (¬pC₂ ∨ pC)
C = C₁ ∨ C₂
(¬pC ∨ ¬pC₁ ∨ pC₂) ∧ (pC₁ ∨ pC) ∧ (pC ∨ ¬pC₂)
C = C₁ → C₂
(¬pC ∨ ¬pC₁ ∨ pC₂) ∧ (¬pC ∨ pC₁ ∨ ¬pC₂) ∧ (pC ∨ ¬pC₁ ∨ ¬pC₂) ∧ (pC ∨ pC₁ ∨ pC₂)
C = C₁ ↔ C₂