Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next 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 11:08] vkuncak |
||
---|---|---|---|
Line 1: | Line 1: | ||
====== Lecture 5 Skeleton ====== | ====== Lecture 5 Skeleton ====== | ||
- | + | Two important techniques: | |
- | + | * Nelson-Oppen combination method | |
- | + | * Resolution | |
===== Basic idea of Nelson-Oppen combination ===== | ===== Basic idea of Nelson-Oppen combination ===== | ||
Line 45: | Line 44: | ||
* the same number of nodes | * the same number of nodes | ||
* same properties on shared symbols (equality and sometimes more) | * same properties on shared symbols (equality and sometimes more) | ||
+ | |||
+ | Lazy approach to integrating solvers for conjunctions and SAT solvers | ||
==== General case ==== | ==== General case ==== | ||
Line 78: | Line 79: | ||
* f(5) | * f(5) | ||
* ALL x. 0 <= x --> f(x) > 0 | * ALL x. 0 <= x --> f(x) > 0 | ||
+ | |||
Line 101: | Line 103: | ||
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 ===== |