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 |