Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
sav08:applications_of_quantifier_elimination [2009/04/22 23:50] vkuncak |
sav08:applications_of_quantifier_elimination [2009/04/23 14:16] vkuncak |
||
---|---|---|---|
Line 9: | Line 9: | ||
we obtain formula | we obtain formula | ||
\[ | \[ | ||
- | x \le z | + | y \le z |
\] | \] | ||
Line 69: | Line 69: | ||
* $F'$ can be (more than) exponentially larger than $F$ | * $F'$ can be (more than) exponentially larger than $F$ | ||
* sometimes quantifiers naturally come up when encoding the problem | * sometimes quantifiers naturally come up when encoding the problem | ||
+ | |||
Line 75: | Line 76: | ||
What class of relations is defined by integer programs without loops in the syntax of [[Simple Programming Language]] ? | What class of relations is defined by integer programs without loops in the syntax of [[Simple Programming Language]] ? | ||
- | ++++| Formulas in Presburger arithmetic. | + | ++++| The class given by formulas in Presburger arithmetic. |
++++ | ++++ | ||