• English only

# Differences

This shows you the differences between two versions of the page.

Link to this comparison view

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 formulaconsider case where R denotes less than relation on integers and Ev denotes that integer is even +More informationChapter 5.of [[Gallier Logic Book]].
-  (ALL xEX 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+

sav07_lecture_5_skeleton.txt · Last modified: 2007/03/28 23:02 by vkuncak

© EPFL 2018 - Legal notice