Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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 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