Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Last revision Both sides next revision | ||
|
sav07_lecture_5_skeleton [2007/03/28 11:08] vkuncak |
sav07_lecture_5_skeleton [2007/03/28 17:57] vkuncak |
||
|---|---|---|---|
| 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 | ||