Tseytin Transformation — Interactive Lab

Formula Input

Operators: ! not | & and | | or | -> implies | <-> iff | Atoms: uppercase letters, true, false

E(C) Transformation Rules

(¬p_C ∨ C) ∧ (¬C ∨ p_C)

C is variable

(¬p_C ∨ ⊤) ∧ (⊥ ∨ p_C)

C is true

(¬p_C ∨ ⊥) ∧ (⊤ ∨ p_C)

C is false

(¬p_C ∨ ¬p_D) ∧ (p_D ∨ p_C)

C = ¬D

(¬p_C ∨ p_C₁) ∧ (¬p_C ∨ p_C₂) ∧ (¬p_C₁ ∨ ¬p_C₂ ∨ p_C)

C = C₁ ∧ C₂

(¬p_C ∨ p_C₁ ∨ p_C₂) ∧ (¬p_C₁ ∨ p_C) ∧ (¬p_C₂ ∨ p_C)

C = C₁ ∨ C₂

(¬p_C ∨ ¬p_C₁ ∨ p_C₂) ∧ (p_C₁ ∨ p_C) ∧ (p_C ∨ ¬p_C₂)

C = C₁ → C₂

(¬p_C ∨ ¬p_C₁ ∨ p_C₂) ∧ (¬p_C ∨ p_C₁ ∨ ¬p_C₂) ∧ (p_C ∨ ¬p_C₁ ∨ ¬p_C₂) ∧ (p_C ∨ p_C₁ ∨ p_C₂)

C = C₁ ↔ C₂