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