Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | |||
|
sav07_lecture_23 [2007/07/02 17:51] simon.blanchoud |
sav07_lecture_23 [2008/05/21 23:14] vkuncak |
||
|---|---|---|---|
| Line 130: | Line 130: | ||
| * First-order theory : $\forall x \exist y . f(f(a,a), x) = f(y, a) \wedge y \neq a$ | * First-order theory : $\forall x \exist y . f(f(a,a), x) = f(y, a) \wedge y \neq a$ | ||
| This is First-Order Logic (FOL) with variables ! We can relate this to set constraints | This is First-Order Logic (FOL) with variables ! We can relate this to set constraints | ||
| + | |||
| Line 168: | Line 169: | ||
| After elimination of the quantifiers, deciding the result of the formula is trivial. | After elimination of the quantifiers, deciding the result of the formula is trivial. | ||
| - | |||
| - | If we add to our language the possibility ot replace $k$ by $card(S)$ then this new language is still decidable and is equivalent to Presbulgarian arithmetic ! | ||