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:
C is the empty clause
(2) Show, using resolution, that
-
A derivation of the empty clause from S is called a refutation of S
Speaker notes:
Content Tools
Tools
Sources (0)
Tags (0)
Comments (0)
History
Usage
Questions (0)
Playlists (0)
Sources
There are currently no sources for this slide.