Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | |||
sav07_lecture_5_skeleton [2007/03/28 17:57] vkuncak |
sav07_lecture_5_skeleton [2007/03/28 23:02] (current) vkuncak |
||
---|---|---|---|
Line 3: | Line 3: | ||
Two important techniques: | Two important techniques: | ||
* Nelson-Oppen combination method | * Nelson-Oppen combination method | ||
- | * Resolution | + | * Proof search |
===== Basic idea of Nelson-Oppen combination ===== | ===== Basic idea of Nelson-Oppen combination ===== | ||
Line 102: | Line 102: | ||
* 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: see next lecture. |
- | Example formula: consider case where R denotes less than relation on integers and Ev denotes that integer is even | + | More information: Chapter 5.4 of [[Gallier Logic Book]]. |
- | (ALL x. EX y. R(x,y)) & | + | |
- | (ALL x y z. R(x,y) --> R(x, plus(x,z))) & | + | |
- | (Ev(x) | Ev(plus(x,1))) --> | + | |
- | (ALL x. EX y. R(x,y) & E(y)) | + | |
- | + | ||
- | From formulas to clauses | + | |
- | * negation normal form | + | |
- | * prenex form | + | |
- | * Skolemization | + | |
- | * conjunctive normal form | + | |
- | + | ||
- | Term model and herbrand theorem. | + | |
- | + | ||
- | Unification as equation solving in term algebra: | + | |
- | * most general unifier | + | |
- | + | ||
- | Resolution and factoring proof rules. | + | |
- | + | ||
- | Theorem prover competition: http://www.cs.miami.edu/~tptp/ | + | |
- | + | ||
- | Hanbdook of Automated Reasoning: http://www.voronkov.com/manchester/handbook-ar/index.html | + | |