Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
sav07_lecture_12_skeleton [2007/04/26 12:58] vkuncak |
sav07_lecture_12_skeleton [2007/04/26 12:59] vkuncak |
||
|---|---|---|---|
| Line 7: | Line 7: | ||
| * formulate standard condition for inductive invariant over templates | * formulate standard condition for inductive invariant over templates | ||
| * eliminate implication using Farkas lemma | * eliminate implication using Farkas lemma | ||
| - | * remove existential [[http://en.wikipedia.org/wiki/Real_closed_field#Decidability_and_quantifier_elimination|quantifiers using quantifier elimination for real fields]] | + | * remove existential quantifiers using [[http://en.wikipedia.org/wiki/Real_closed_field#Decidability_and_quantifier_elimination|quantifier elimination for real fields]] |
| Quantifier elimination does not scale in general. Some improvements: | Quantifier elimination does not scale in general. Some improvements: | ||