Differences

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

--- 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:
   * Nelson-Oppen combination method
-  * Resolution
+  * Proof search
 ===== Basic idea of Nelson-Oppen combination =====
@@ Line 102: / Line 102: @@
   * 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