Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | |||
sav08:introductory_remarks_on_smt_provers [2009/05/06 09:46] vkuncak |
sav08:introductory_remarks_on_smt_provers [2015/04/21 17:30] (current) |
||
---|---|---|---|
Line 30: | Line 30: | ||
Consider the following formula, where $f$ denotes functions from integers to integers and $a,b$ are integers. | Consider the following formula, where $f$ denotes functions from integers to integers and $a,b$ are integers. | ||
- | \[\begin{array}{l} | + | \begin{equation*}\begin{array}{l} |
(\forall x.\forall y.\ x \le y \rightarrow f(x) \le f(y))\ \land \\ | (\forall x.\forall y.\ x \le y \rightarrow f(x) \le f(y))\ \land \\ | ||
(\forall x.\forall y. f(x)=f(y) \rightarrow x=y)\ \land\\ | (\forall x.\forall y. f(x)=f(y) \rightarrow x=y)\ \land\\ | ||
Line 36: | Line 36: | ||
b < a | b < a | ||
\end{array} | \end{array} | ||
- | \] | + | \end{equation*} |
Is this formula satisfiable? | Is this formula satisfiable? | ||
* over integers ++|No. Why?++ | * over integers ++|No. Why?++ | ||
* over reals ++|Yes. Why?++ | * over reals ++|Yes. Why?++ | ||