LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision 		Previous revision
sav07_lecture_5_skeleton [2007/03/28 11:08]
vkuncak 		sav07_lecture_5_skeleton [2007/03/28 23:02]
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 25: Line 25:
 Preservation of loop invariant: prove validity of Preservation of loop invariant: prove validity of
   (ALL i. 0 <= i & i < n --> a(j) > 0) -->   (ALL i. 0 <= i & i < n --> a(j) > 0) -->
-  (ALL i. 0 <= i & i < n+1 --> a(n:=1)(j) > 0)+  (ALL i. 0 <= i & i < n+1 --> a(n:=1)(i) > 0)
  
 or satisfiability of or satisfiability of
  
   (ALL i. 0 <= i & i < n --> a(i) > 0) &    (ALL i. 0 <= i & i < n --> a(i) > 0) & 
-  (EX i. 0 <= i & i < n+1 & a(n:=1)(j) >= 0)+  (EX i. 0 <= i & i < n+1 & a(n:=1)(i) <= 0)
  
 Let us prove a weaker quantifier-free property (by skolemizing and instantiating the quantifier):​ Let us prove a weaker quantifier-free property (by skolemizing and instantiating the quantifier):​
  
   (0 <= i & i < n --> a(i) > 0) &    (0 <= i & i < n --> a(i) > 0) & 
-  0 <= i & i < n+1 & a(n:​=1)(i) ​>= 0+  0 <= i & i < n+1 & a(n:​=1)(i) ​<= 0
  
 Soundness in example. Soundness in example.
Line 56: Line 56:
  
 The harder part: proving that it is complete. The harder part: proving that it is complete.
- 
  
 Using a SAT solver to enumerate disjunctive normal form disjuncts. Using a SAT solver to enumerate disjunctive normal form disjuncts.
Line 65: Line 64:
  
 For more details, see [[http://​verify.stanford.edu/​summerschool2004|Combination of Decision Procedures Summer School 2004]]. For more details, see [[http://​verify.stanford.edu/​summerschool2004|Combination of Decision Procedures Summer School 2004]].
- 
- 
- 
  
 ==== Quantifier instantiation ==== ==== Quantifier instantiation ====
  
-  * Basic idea, and in the above example+  * Basic idea, and in the above example ​(name i from the EX i as i0, then instantiated ALL i also with i=i0)
   * examples of incompleteness:​   * examples of incompleteness:​
  
Line 79: Line 75:
   * f(5)   * f(5)
   * ALL x. 0 <= x --> f(x) > 0   * ALL x. 0 <= x --> f(x) > 0
- 
- 
  
  
Line 94: Line 88:
  
 Proof rules for first-order logic. Proof rules for first-order logic.
-   * propositional axioms +   * propositional axioms: an instance of propositional tautology is an axiom 
-   * instantiation +   * instantiation: from (ALL x.F) derive F[x:=t]. 
-   * generalization+   * generalization: after proving F which contains a fresh variable x, conclude (ALL x.F)
  
 Example: axiomatizing some set operations. Example: axiomatizing some set operations.
-Axiomatization ​of equality.+Recall also axiomatization ​of equality.
  
-Two different techniques ​(recall we can take negation of formulas):+We have seen two different techniques:
   * 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: semi decision procedure (complete but non-terminating)   * 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: ​see next lecture.
- +
-Example formula: consider case where R denotes less than relation on integers and Ev denotes that integer is even +
-  (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+More information: Chapter 5.4 of [[Gallier Logic Book]].