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
sav08:arrays_are_functions [2008/04/23 14:44]
vkuncak
sav08:arrays_are_functions [2008/04/23 14:45] (current)
vkuncak
Line 1: Line 1:
 ====== Arrays are Functions ====== ====== Arrays are Functions ======
  
-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]]
  
 
sav08/arrays_are_functions.txt · Last modified: 2008/04/23 14:45 by vkuncak
 
© EPFL 2018 - Legal notice