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:arrays_are_functions [2008/04/23 09:18]
vkuncak
sav08:arrays_are_functions [2008/04/23 14:45]
vkuncak
Line 1: Line 1:
 ====== Arrays are Functions ====== ====== Arrays are Functions ======
  
-Sometimes people consider thory of arrays.  ​A simple theory of arrays is obtained if we simply allow function update expressions in FOL, as in [[FOL with Update Expressions]]. +A simple theory of arrays is obtained if we simply allow function update expressions in FOL, as in [[FOL with Update Expressions]].  As we explained there, this theory can be reduced to FOL.  The reduction does not introduce quantifiers,​ so we obtain decidability for quantifier-free theory of arrays
-  * textbook section +  * [[Calculus of Computation Textbook]] Section 9.5 
-  * UCLID decision procedure+  * [[http://​citeseer.ist.psu.edu/​650776.html|The ​UCLID Decision Procedure]]