Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:introductory_remarks_on_smt_provers [2009/05/06 09:45] vkuncak |
sav08:introductory_remarks_on_smt_provers [2009/05/06 09:46] vkuncak |
||
---|---|---|---|
Line 25: | Line 25: | ||
Note: formulas that are valid in the combination of quantifiers, linear integers, and uninterpreted functions are not enumerable (and neither are formulas that are not valid). The situation is worse than in pure first-order logic. | Note: formulas that are valid in the combination of quantifiers, linear integers, and uninterpreted functions are not enumerable (and neither are formulas that are not valid). The situation is worse than in pure first-order logic. | ||
+ | |||
===== Example ===== | ===== Example ===== | ||
Line 36: | Line 37: | ||
\end{array} | \end{array} | ||
\] | \] | ||
- | Is this formula satisfiable? ++|yes. Why?++ | + | Is this formula satisfiable? |
+ | * over integers ++|No. Why?++ | ||
+ | * over reals ++|Yes. Why?++ |