Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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