Current Slide
Small screen detected. You are viewing the mobile version of SlideWiki. If you wish to edit slides you will need to use a larger device.
Converting to clausal form
Theorem : Every propositional formula can be transformed into an equivalent formula in CNF
1. Implications:
φ1 → φ2 → ¬φ1 ∨ φ2
φ1 ← φ2 → φ1 ∨ ¬φ2
φ1 ↔ φ2 → (¬φ1 ∨ φ2 ) ∧ (φ1 ∨ ¬φ2)
2. Negations:
¬¬φ → φ
¬(φ1 ∧ φ2 ) → ¬φ1 ∨ ¬φ2
¬(φ1 ∨ φ2 ) → ¬φ1 ∧ ¬φ2
3. Distribution:
φ1 ∨ (φ2 ∧ φ3 ) → (φ1 ∨ φ2) ∧ (φ1 ∨ φ3 )
(φ1 ∧ φ2) ∨ φ3 → (φ1 ∨ φ3 ) ∧ (φ2 ∨ φ3)
(φ1 ∨ φ2) ∨ φ3 → φ1 ∨ (φ2 ∨ φ3)
(φ1 ∧ φ2) ∧ φ3 → φ1 ∧ (φ2 ∧ φ3)
4. Operators:
φ1 ∨... ∨ φn → {φ1,...,φn}
φ1 ∧ ...∧ φn → {φ1}...{φn}
