Topics
#formulatree#cnf#rewriting#tseitin#nicknames#equisat

CNF & Tseitin Transformation

Ready
Rules at a glance

Rewriting (same meaning)

1. φ ↔ ψ ⇒ (φ → ψ) ∧ (ψ → φ) 2. φ → ψ ⇒ ¬φ ∨ ψ 3. push ¬ down, ¬¬φ ⇒ φ 4. φ ∨ (ψ ∧ χ) ⇒ (φ ∨ ψ) ∧ (φ ∨ χ). Clean up: drop clauses with x and ¬x. Can explode.

Nicknames / Tseitin (same answer)

While it is not a checklist: pick a simple piece χ (only atoms below it), give it a fresh name t, write the rules of t ↔ χ, fold every copy of χ into t. Stop as soon as the rest is a checklist.

Rules of t ↔ χ

¬a: (¬t ∨ ¬a) (t ∨ a) · a ∧ b: (¬t ∨ a) (¬t ∨ b) (¬a ∨ ¬b ∨ t) · a ∨ b: (¬t ∨ a ∨ b) (¬a ∨ t) (¬b ∨ t) · a → b: (¬t ∨ ¬a ∨ b) (a ∨ t) (¬b ∨ t) · a ↔ b: 4 clauses.