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.