This is an old revision of the document!
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.
- textbook section
- UCLID decision procedure