Choices in the semantics and the signature of a theory are integral in determining how the theory is used and how challenging it is to reason over it. Our interest in this paper lies in the SMT theory of sequences. Various versions of it exist in the literature and in state-of-the-art SMT solvers, but it has not yet been standardized in the SMT-LIB. We reflect on its existing variants, and we define a set of theory design criteria to help determine what makes one variant of a theory better than another. The criteria we define can be used to appraise theory proposals for other theories as well. Based on these criteria, we propose a series of changes to the SMT theory of sequences as a contribution to the discussion regarding its standardization.

翻译：理论语义与符号的选择对于确定其应用方式及推理难度具有决定性影响。本文聚焦于SMT中的序列理论。当前文献与前沿SMT求解器中存在该理论的多种变体，但尚未在SMT-LIB标准中实现规范化。本文系统梳理现有变体，并提出一套理论设计准则以评估不同理论变体的优劣。所定义的准则同样适用于其他理论方案的评估。基于这些准则，我们针对SMT序列理论提出一系列改进建议，旨在推动其标准化进程的讨论。