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 11:00]
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.
   * [[Calculus of Computation Textbook]] Section 9.5   * [[Calculus of Computation Textbook]] Section 9.5
   * [[http://​citeseer.ist.psu.edu/​650776.html|The UCLID Decision Procedure]]   * [[http://​citeseer.ist.psu.edu/​650776.html|The UCLID Decision Procedure]]