# Differences

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

 sav08:introductory_remarks_on_smt_provers [2009/05/06 09:45]vkuncak sav08:introductory_remarks_on_smt_provers [2015/04/21 17:30] (current) Both sides previous revision Previous revision 2009/05/06 09:46 vkuncak 2009/05/06 09:45 vkuncak 2009/05/06 09:45 vkuncak 2009/05/06 09:43 vkuncak 2009/05/06 09:25 vkuncak 2009/05/06 00:24 vkuncak 2009/05/06 00:24 vkuncak 2009/05/06 00:24 vkuncak 2008/04/17 11:37 vkuncak 2008/04/17 11:08 vkuncak 2008/04/17 11:08 vkuncak 2008/04/17 11:06 vkuncak 2008/04/17 11:06 vkuncak 2008/04/17 11:05 vkuncak 2008/04/17 10:45 vkuncak 2008/04/17 10:29 vkuncak 2008/04/17 10:28 vkuncak 2008/04/17 10:27 vkuncak created Next revision Previous revision 2009/05/06 09:46 vkuncak 2009/05/06 09:45 vkuncak 2009/05/06 09:45 vkuncak 2009/05/06 09:43 vkuncak 2009/05/06 09:25 vkuncak 2009/05/06 00:24 vkuncak 2009/05/06 00:24 vkuncak 2009/05/06 00:24 vkuncak 2008/04/17 11:37 vkuncak 2008/04/17 11:08 vkuncak 2008/04/17 11:08 vkuncak 2008/04/17 11:06 vkuncak 2008/04/17 11:06 vkuncak 2008/04/17 11:05 vkuncak 2008/04/17 10:45 vkuncak 2008/04/17 10:29 vkuncak 2008/04/17 10:28 vkuncak 2008/04/17 10:27 vkuncak created 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 ===== 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 35: Line 36: b < a b < a \end{array} \end{array} -$ + \end{equation*} - Is this formula satisfiable?​ ++|No. Why?++ + Is this formula satisfiable?​ + * over integers  ​++|No. Why?++ + * over reals  ++|Yes. Why?++