Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
sav07_lecture_5_skeleton [2007/03/28 10:50] vkuncak |
sav07_lecture_5_skeleton [2007/03/28 10:51] vkuncak |
||
|---|---|---|---|
| Line 78: | Line 78: | ||
| * f(5) | * f(5) | ||
| * ALL x. 0 <= x --> f(x) > 0 | * ALL x. 0 <= x --> f(x) > 0 | ||
| + | |||
| Line 101: | Line 102: | ||
| Two different techniques (recall we can take negation of formulas): | Two different techniques (recall we can take negation of formulas): | ||
| * Enumerating finite models (last time) gives us a way to show formula is satisfiable | * Enumerating finite models (last time) gives us a way to show formula is satisfiable | ||
| - | * Enumerating proofs gives us a way to show that formula is valid | + | * Enumerating proofs gives us a way to show that formula is valid: semi decision procedure (complete but non-terminating) |
| The gap in the middle: invalid formulas with only infinite models | The gap in the middle: invalid formulas with only infinite models | ||
| * an example with only infinite models: strict partial order with no upper bound | * an example with only infinite models: strict partial order with no upper bound | ||
| - | |||
| - | |||
| - | |||
| - | |||
| - | |||
| ===== Resolution theorem proving ===== | ===== Resolution theorem proving ===== | ||