Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
sav08:non-ground_instantiation_and_resolution [2008/04/01 17:45] vkuncak |
sav08:non-ground_instantiation_and_resolution [2008/04/01 20:08] vkuncak |
||
|---|---|---|---|
| Line 31: | Line 31: | ||
| Illustration of rules. | Illustration of rules. | ||
| - | ===== Reducing the Search Space ===== | + | ===== Combining Instantiation and Resolution ===== |
| - | More powerful rules. | + | These two are more powerful rules. |
| - | But more choices at each step. | + | But we therefore have more choices at each step. |
| If we try to do the proof, how do we know what to instantiate with? ++|we instantiate to enable subsequent resolution rule.++ | If we try to do the proof, how do we know what to instantiate with? ++|we instantiate to enable subsequent resolution rule.++ | ||