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_homework_4 [2007/04/24 22:22] vkuncak |
sav07_homework_4 [2007/04/24 22:22] vkuncak |
||
|---|---|---|---|
| Line 141: | Line 141: | ||
| You can find some example formulas in jahob/examples/nasty_formulas directory of Jahob. | You can find some example formulas in jahob/examples/nasty_formulas directory of Jahob. | ||
| + | |||
| Line 202: | Line 203: | ||
| The solution is therefore to first flatten expressions by introducing fresh variables for all IF expressions and then transform IF expressions into disjunctions and conjunctions. When proving validity of formulas, we can obtain, for example: | The solution is therefore to first flatten expressions by introducing fresh variables for all IF expressions and then transform IF expressions into disjunctions and conjunctions. When proving validity of formulas, we can obtain, for example: | ||
| - | (v1 = (if i=i then o1 else a(i))) & | + | (v1 = (if i=i then o1 else a(i))) & |
| - | v2 = (if i=i+k then o2 else v2) & | + | v2 = (if i=i+k then o2 else v2) & |
| - | v3 = (if i+k=i then o1 else a(i+k)) & | + | v3 = (if i+k=i then o1 else a(i+k)) & |
| - | v4 = (if i+k=i+k then o2 else v3)) --> v2 = v4 | + | v4 = (if i+k=i+k then o2 else v3)) --> v2 = v4 |
| You can generate such formulas by repeatedly extracting the innermost IF expressions and naming them using fresh variables. If you have such a set of definitions of the form v1=t1, ..., vn=tn then if you are proving validity of formula F you use | You can generate such formulas by repeatedly extracting the innermost IF expressions and naming them using fresh variables. If you have such a set of definitions of the form v1=t1, ..., vn=tn then if you are proving validity of formula F you use | ||