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 (cont’)

  • Example: Show that (p → q) → (¬q → ¬p) is a valid formula
    Solution: We will show that  

    ¬[(p → q) → (¬q → ¬p)]

    is not satisfiable.

    (1) Transform the formula into CNF:

    (2) Show, using resolution, that

    3. C is the empty clause

  • A derivation of the empty clause from S is called a refutation of S


Speaker notes:

Content Tools

Sources

There are currently no sources for this slide.