The SMT (Satisfiability Modulo Theories) theory of arrays is well-established and widely used, with variousdecision procedures and extensions developed for it. However, recent works suggest that developing tailoredreasoning for some theories, such as sequences and strings, is more efficient than reasoning over them throughaxiomatization over the theory of arrays. In this paper, we are interested in reasoning over n-indexed sequences asthey are found in some programming languages, such as Ada. We propose an SMT theory of n-indexed sequencesand explore different ways to represent and reason over n-indexed sequences using existing theories, as well astailored calculi for the theory.

翻译：数组的可满足性模理论（SMT）理论已十分成熟且应用广泛，并已为其开发了多种决策过程与扩展。然而，近期研究表明，针对某些理论（如序列和字符串）开发定制化的推理方法，比通过数组理论的公理化进行推理更为高效。本文关注于对某些编程语言（如Ada）中出现的n索引序列进行推理。我们提出了一种n索引序列的SMT理论，并探讨了利用现有理论表示和推理n索引序列的不同方法，以及针对该理论的定制演算。