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_3_skeleton [2007/03/21 11:04] vkuncak |
sav07_lecture_3_skeleton [2007/03/21 12:28] vkuncak |
||
|---|---|---|---|
| Line 177: | Line 177: | ||
| T ::= var | T + T | K * T (terms) | T ::= var | T + T | K * T (terms) | ||
| A ::= T=T | T <= T (atomic formulas) | A ::= T=T | T <= T (atomic formulas) | ||
| - | F ::= F & F | F|F | ~F (formulas) | + | F ::= A | F & F | F|F | ~F (formulas) |
| To get full Presburger arithmetic, allow existential and universal quantifiers in formula as well. | To get full Presburger arithmetic, allow existential and universal quantifiers in formula as well. | ||
| Line 243: | Line 243: | ||
| * Presburger Arithmetic (PA) bounds: {{papadimitriou81complexityintegerprogramming.pdf}} | * Presburger Arithmetic (PA) bounds: {{papadimitriou81complexityintegerprogramming.pdf}} | ||
| * Specializing PA bounds: http://www.lmcs-online.org/ojs/viewarticle.php?id=43&layout=abstract | * Specializing PA bounds: http://www.lmcs-online.org/ojs/viewarticle.php?id=43&layout=abstract | ||
| - | |||
| - | |||
| - | |||
| - | |||