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_homework_2 [2007/03/29 22:13] vkuncak |
sav07_homework_2 [2007/03/29 22:19] vkuncak |
||
---|---|---|---|
Line 1: | Line 1: | ||
====== Homework 2 ====== | ====== Homework 2 ====== | ||
+ | |||
Line 22: | Line 23: | ||
For in depth understanding you can also read references in there, in particular the relevant Wilfrid Hodges model theory book sections. | For in depth understanding you can also read references in there, in particular the relevant Wilfrid Hodges model theory book sections. | ||
- | + | **Hint**: You should be able to reduce the problem to reasoning about conjunctions and generate a disjunction over total orders over terms of form v+c. Alternatively, you may be able to use some ideas of [[http://citeseer.ist.psu.edu/71579.html|Fourier-Motzkin elimination]]. | |
- | + | ||
==== Verification condition generator ==== | ==== Verification condition generator ==== |