Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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 [2015/04/21 17:30] (current)
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?++ 
 
sav08/introductory_remarks_on_smt_provers.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice