We present a first-order theory of (finite) sequences with integer elements, Presburger arithmetic, and regularity constraints, which can model significant properties of data structures such as lists and queues. We give a decision procedure for the quantifier-free fragment, based on an encoding into the first-order theory of concatenation; the procedure has PSPACE complexity. The quantifier-free fragment of the theory of sequences can express properties such as sortedness and injectivity, as well as Boolean combinations of periodic and arithmetic facts relating the elements of the sequence and their positions (e.g., "for all even i's, the element at position i has value i + 3 or 2i"). The resulting expressive power is orthogonal to that of the most expressive decidable logics for arrays. Some examples demonstrate that the fragment is also suitable to reason about sequence-manipulating programs within the standard framework of axiomatic semantics.
McCarthy initiated the research on formal reasoning about arrays @cite_15 . His theory of arrays defines the axiomatization of the basic access operations of and for quantifier-free formulas and without arithmetic or extensionality (i.e., the property that if all elements of two arrays are equal then the arrays themselves are equal). McCarthy's work has usually been the kernel of every theory of arrays: most works on (automated) reasoning about arrays extend McCarthy's theory with more complex (decidable) properties or efficiently automate reasoning within an existing theory.
@cite_15
2124141583
In this paper I shall discuss the prospects for a mathematical science of computation. In a mathematical science, it is possible to deduce from the basic assumptions, the important properties of the entities treated by the science. Thus, from Newton’s law of gravitation and his laws of motion, one can deduce that the planetary orbits obey Kepler’s laws.