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}


Speaker notes:

Content Tools

Sources

There are currently no sources for this slide.