LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

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?++