Recently, symbolic structures were proposed as finite representations of potentially infinite first-order structures, where Linear Integer Arithmetic terms and formulas define the domain and interpretations of a structure. We generalize symbolic structures to use any base theory that admits a standard model. Symbolic structures induce a symbolic model property, which holds for a fragment of first-order logic if every satisfiable formula in the fragment has a symbolic model. The symbolic model property implies decidability, since the model-checking problem for symbolic structures is decidable. We use the symbolic model property to prove decidability for several fragments that extend the fragment of stratified formulas, relaxing the quantifier-alternation constraints by allowing one sort to have self-looping functions, under certain restrictions. To establish the symbolic model property for these fragments we construct a symbolic model for a formula from an arbitrary model. The construction and its correctness are proved in a generic fashion, which may be instantiated to other similarly restricted fragments.

翻译：近期，符号结构被提出作为潜在无限一阶结构的有限表示形式，其中线性整数算术项与公式定义了结构的论域及解释。本文将符号结构推广至任意可容许标准模型的基础理论。符号结构诱导出一种符号模型性质，该性质对一阶逻辑片段成立的条件是：该片段中每个可满足公式均存在符号模型。由于符号结构的模型检验问题具有可判定性，符号模型性质蕴含片段的可判定性。本文利用符号模型性质证明若干扩展分层公式片段的可判定性——通过允许特定限制下某类具有自循环函数的排序，放松了量词交替约束。为建立这些片段的符号模型性质，我们基于任意模型为公式构造符号模型。该构造及其正确性证明以通用化形式给出，并可实例化至其他类似受限的片段。