Differences
This shows you the differences between two versions of the page.
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]] |