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.

Resolution - Converting to Clause Normal Form

  • Resolution expects input in clause normal form
  • Step 1: Eliminate the logical connectives → and ↔
    • a ↔ b = (a → b) ∧ (b → a)
    • a → b = ¬ a ∨ b
  • Step 2: Reduce the scope of negation
    • ¬ ( ¬ a) = a
    • ¬ (a ∧ b) = ¬ a ∨ ¬ b
    • ¬ (a ∨ b) = ¬ a ∧ ¬ b
    • ¬ ( ∃ X) a(X) = ( ∀ X) ¬ a(X)
    • ¬ ( ∀ X) b(X) = ( ∃ X) ¬ b(X)

Speaker notes:

Content Tools

Sources

There are currently no sources for this slide.