非稳定无穷大与非一阶理论的组合决策过程统一化及其应用.

理论计算机科学电子笔记125（2005）37-51www.elsevier.com/locate/entcs结合非稳定无限，非一阶理论1Pascal Fontaine2 Pascal Gribomont3UniversityofLi`ege（Belgium）摘要并发程序断言验证的一个关键步骤是确定某些文字集是否是可满足的。在这种情况下，Nelson-Oppen组合方案经常使用。该方案将两个不相交的理论的决策过程合并为一个关于这些理论的联合的决策过程。然而，标准版的纳尔逊-奥本技术只处理一种排序的、稳定的有限一阶理论。该方案以前已经适应了许多排序的框架[10]，并处理非稳定的有限理论[9]。这两项改进是单独提出的。我们提出了一个统一的版本，在前两个的连续性，这进一步放宽了稳定无限的要求。 值得注意的是，一些非稳定无限理论现在可以与数组理论相结合。此外，这里使用理论的语义概念提出组合方案，允许处理非一阶理论。关键词：组合，决策过程，非稳定无穷大，非一阶纳尔逊-奥本组合框架[6]旨在从每个理论中的无量化器片段的决策过程中创建一个关于不相交语言的两个理论的联合的决策过程例如，文字L={x≤y，y≤x+f（x），P（h（x）−h（y）），<$P（0），f（x）= 0}包含未解释的谓词和用整数线性算术扩充的函数。该组合方案从未解释谓词的决策过程中为这样的文字集1这一点是根据“C om m un aut′efrann cchei s e de Be l g i que- D i r e c t i o n de la re che r ch e scin i fique- A c t i o n s de re c h e r c h e n c e r t ′ e s“的规定提出的2电子邮件：pfontain@montefiore.ulg.ac.be3 电子邮件地址：gribomont@montefiore.ulg.ac.be1571-0661 © 2005 Elsevier B.V. 在CC BY-NC-ND许可证下的O笔访问。doi：10.1016/j.entcs.2004.06.06638P. Fontaine，P.Gribomont/Electronic Notes in Theoretical Computer Science 125（2005）37和功能（即，空一阶理论）和线性算术的决策过程。这是可能的，因为语言是不相交的，唯一共享的符号是等式和变量。Nelson-Oppen组合格式通常作为一阶理论的组合格式提出。然而，采用更语义化的观点可以避免处理诸如“理论”之类的微妙问题只允许任意大的有限模型4通过精确地选择模，这是一个人想要思考的“理论”。一个I-理论是对所考虑的语言的一组任意的解释。例如，考虑整数上的线性算术，I-理论将是所有解释的集合，这些解释对应于将集合分配给定义域的单一结构，以及它们对符号+、−、≤、0、1的通常意义。. . 我们在这里提出一个I-理论的组合 由于一阶理论可以表示为I-理论，因此，可以看作是一个推广的一阶纳尔逊-奥本组合阴谋具有类似广义理论概念的Shostak在验证上下文中，在多排序框架中表达验证条件是很自然的[3]。最近，Nelson-Oppen方法在有序框架中被重新表述并证明是正确的[10]。为了简化演示，我们宁愿在一个基本的多排序框架中工作，使用不相交的排序（即，没有子分类）。传统上，要求组合中的理论是稳定无限的。这意味着使用组合方案对于一些常见的理论（特别是那些只有有限模型的理论）是有问题的。在[9]的哲学中，我们将证明，在一个多分类的框架中，非稳定无限理论很容易与一些非常有用的理论（特别是空理论和数组理论）结合起来1预赛一个多序一阶语言是一个元组L=S，V，F，P，r，d，使得S是一个可数的非空的排序（或类型）集，V是排序τ的变量的不相交可数集Vτ的（可数）并集，F是一个可数无限的函数符号集，P是一个可数无限的谓词符号集，r给F中的每个函数符号和P中的每个谓词符号分配一个元数，d给每个函数符号f ∈F分配一个Sr（f）+1中的排序，给每个函数符号f ∈ F分配一个S r（f）+1中的排序，给每个函数符号f ∈ F分配一个S r（f）+1Sr（p）对每个谓词符号p∈ P。空谓词是命题，[4]一个允许任意大的有限模型的一阶理论也有无限模型。[5]对应于一阶理论的I-理论只是一阶理论的模型的集合。P. Fontaine，P.Gribomont/Electronic Notes in Theoretical Computer Science 125（2005）3739空值函数是常量。L的子集是一种多排序语言，使得排序、变量、函数和谓词符号的集合是L的相应集合的子集。假设符号没有重载。也就是说，一个给定的函数或谓词不能分配给不同的排序。然而，对不同种类的参数使用相同的符号是方便的。在这种情况下，它表面上认为，这些符号是隐含的“装饰”与他们的排序声明。一个例子是相等符号“="，它被装饰成一个符号用于每一个排序。多排序语言的项、原子（原子公式）、文字和公式都以通常的方式定义。一个公式在多排序一阶语言L中的解释是一个对I= D，I，其中D为每个排序τ ∈ S分配一个非空域Dτ，而I为每个变量、函数和谓词符号分配一个含义。像往常一样，单位被分配给相等符号。一种解释是在D τ中对I[t]的一种解释，以everyytertofsortτ。类似地，解释I在{T，T}中具有值I [k]，以针对多个值进行平均。 如果I[k] =T，则I的不确定性对于多个k是一种改进。 我不知道你在说什么。语言L中的一个解释I到L的一个子集的一个重新定义是对于L的子集中的每个域、函数符号、谓词符号，等于I的解释。一阶理论是一组公理，它定义了一组解释，即，一阶理论的模型。一个自然的扩展是考虑I-理论：一个I-理论是一个给定的多排序语言的任意解释集。对应于一阶理论的I-理论是一阶理论的模型的集合。一个I-理论可能会留下一些谓词和未解释的功能 一个谓词p的排序是<$τ1，. τn（排序为ττ1的函数f，.τn，τ n）在一个I-理论T中是不可解释的，如果对于每个解释，I= D，I∈ T，并且对于每个谓词q（分别为.函数g）有一个解释IJ∈ T使得IJ与I相同，除了IJ[p]=q（re sp. I J[f]=g）。假设这些变量都是线性的，在任何I-理论中都是未解释的，其意义类似于未解释的常数。给定一个I-理论T，一个公式T是T-可满足的，如果它在T中有一个模型。两个I-理论是不相交的，如果它们的语言是不相交的。不相交语言是具有不相交的函数（和常量）和谓词集合的语言（尽管相等符号是共享的）。两个不相交的I-理论的谓词和函数的公式是用不相交语言的联合写成的。不相交的结合语言L1=<$S1，V1，F1，P1，r1，d1<$n和L2=<$S2，V2，F2，P2，r2，d2<$n 是 多 排 序 语 言 L =<$S1<$S2 ， V1<$V2 ， F1<$F2 ， P1<$P2 ， r ，d<$n，其中r是当其参数在r1的域中时等于r 1的函数，否则等于r2。函数d的定义类似。40P. Fontaine，P.Gribomont/Electronic Notes in Theoretical Computer Science 125（2005）37JJ1n1n1n1n不相交语言L1和L2的并集L中的I-理论T可以看作是两个不相交I-理论的并集：T对每个语言Li的限制Ti，即，T中的解释对Li的所有限制的集合。但据更方便的是把I-理论的联合定义为：定义1.1联合T 不相交语言中的I-理论T1和T2L1和L2是所有解释I的集合，使得解释Ii=对于i = 1，2，存在<$Di，I i <$∈ Ti，其中Ii是I对Li的限制.在这个定义中，对T的L1的限制不一定是T1。 的确，如果对L1和L2中公共排序τ，来自T1的解释I1赋予τ一个从未被T2中的任何解释赋予的域，则T中的任何解释都不会有I1作为限制。注意，如果T1和T2是一阶理论T1和T2的模型集合，那么I-理论T1和T2的并集就是对应于公理集T1<$T2的（一阶）理论的模型集合。I理论的定义和我-理论的联合扩展了理论和理论的联合的经典定义，但并不与它们相矛盾由于我们提出的组合方法适用于前面介绍的I-理论的一般概念，因此有必要将“可组合性质”封装在一个新的概念中。将两个不相交的I-理论的决策过程结合起来，要求对于每个公共排序，至少有一个I-理论是不灵活的：定义1.2多排序语言L中的I-理论T在排序τ上是可伸缩的，如果τ不是L的排序，或者如果对于T中的任何解释I= D，I，任何解释IJ=DJ，IJ，使得• 集合Dτ和DJ具有相同的基数，并且对于任何τ τ，DτJ= DJ。τJτ函数b定义从集合Dτ到Dτ的双射，并且是DτJ上的恒等式对于任何τJ/=τ;• 对任意yva可解x，IJ[x]=b（I[x]）;• 对任意函数ymbolf∈F，I J[f]（b（d）， . . b（d））=b（I[f]（d， . .（d））;• 对任意给定的symbolp∈P，I J[p]（b（d）， . . b（d））I[p]（d， . . .d）;也属于T.直观地说，它意味着术语被分配给域中的元素模置换。 它允许将经典组合方案的使用扩展到不一定对应于一阶理论的I-理论。由于只需要一个I-理论是可解的，如果两个I-理论中的一个对应于一阶理论，则直接满足要求：P. Fontaine，P.Gribomont/Electronic Notes in Theoretical Computer Science 125（2005）3741定理1.3如果I-理论T是一个给定语言L中一阶理论的模型集合，则T在每个排序上都是可解的。当组合两个以上的I-理论时，似乎“不确定性要求”将把除了一个I-理论之外的所有I-理论强加在组合中，以对应于一阶理论。幸运的是，情况并非如此。下面的定理表明，如果任何两个独立的非易变性I-理论具有不同的种类，则不存在限制：定理1.4设T 是不相交的I-理论T1和T2的并集。 如果T1和T2在τ上可伸缩，则T在τ上可伸缩。在本章开头的小例子中，文字的集合L是不令人满意的，L1=L2也是如此，L1={x≤y，y≤x+v1，v1=0，v2=v3−v4，v5=0}L2={P（v2），<$P（v5），v1= f（x），v3= h（x），v4= h（y）}。但在Li（i= 1， 2）中的每一个文字都包含函数（和常数），并且只从一个I-理论中产生。L1中的每个文字都是人工语言，而L2中的每个文字都是未解释的谓词和函数的语言共享符号仅是变量（和相等）。集合L1和L2可以通过引入新的变量从L构建一对文字集合（L1，L2）是不相交语言L1和L2的并集中文字L的有限集合的分离，如果：第一，L是T-可满足的当且仅当L1<$L2是T-可满足的;第二，Li是语言Li中文字的有限集合，i= 1， 2。唯一共享的符号是变量符号（和等式）。事实上，给定两种语言和这些语言的联合中的一组文字，总是可以使用变量抽象来构建分离。给定有限个变量集合{x1，. xn}，则C诱导的排列是C的同类中同类变量之间的所有等式的集合，以及C的两个不同类中同类两个变量之间的所有不等式的集合。例如，由划分{{x1，x2}，{x3}}诱导的三个相同排序的变量x1，x2，x3的排列是{x1= x2，x1/= x3，x2/= x3}。事实上，最后一个不等式并不重要：文字集{x1=x2，x1/=x3}在逻辑上等价于前面的排列。2决定程序下面的定理为组合过程提供了抽象的基础。随着对I-理论的进一步要求，它将允许将两个不相交语言的决策过程合并为一个语言的联合42P. Fontaine，P.Gribomont/Electronic Notes in Theoretical Computer Science 125（2005）37定理2.1设语言L中的I-理论T是不相交语言L1和L2中的I-理论T1和T2的并集。 对于每一种排序，T1或T2都是可伸缩的。设L是L上的一组文字，（L1，L2）是L根据L1和L2的分离。设V是L1和L2中公共变量的集合.假设6，对于Li中的每个域τ和L2−i存在等式x = t∈L2−i其中x是V j中的变量。文字集L是T-可满足的当且仅当存在V <$V J的排列A和A <$L i的Ti-模型Ii（i= 1，2），使得对于L1和L2中的任何公共排序τ，与I1和I2中的τ相关联的域具有相同的基数。 在这种情况下，A ∈ L1∈ L2是T-可满足的。证据 证 据 可在附录A中找到。Q解决基数约束（如定理6中的约束）的经典方法是只考虑有限理论中的稳定性。在一个多排序的上下文中，这意味着两个理论相对于公共排序的集合应该是稳定无限的。定义2.2多排序语言L中的I-理论T相对于排序集S是稳定无穷的，如果L上的每个文字L的T-可满足基集都有一个T-模型，为L中使用的每个排序τ ∈ S分配一个基数为0的域。许多有用的I-理论是稳定无限的：整数线性算术的I-理论，对应于数组[8]或列表[7]的一阶理论的I-理论，等等。还可以看到，当谈论一阶理论的模型集合时，Lüowenheim-SkolemTheorem7都放松了这个定义中关于域基数的条件：基数应该大于或等于0。但这仍然是一个非常严格的要求。值得注意的是，它阻止了I-理论与有限域的结合。我们宁愿采取实用主义的观点，特别是研究两个I-理论。相容的I-理论是不需要定理6中的“基数子句”的I-理论定义2.3多类语言L1和L2中的两个不相交的I-理论T1和T2是相容的，如果对于每个分离（L1，L2）和排列A，使得• V是L1和L2中的公共符号的集合;[6]每一个分离都可以转化为一个证明这个条件的分离。[7]Lüwenheim-Skolem的一种模拟方法。在[10]中可以找到用于对数据进行排序的数据集。P. Fontaine，P.Gribomont/Electronic Notes in Theoretical Computer Science 125（2005）3743• 对于Li中的每个类τ和L2−i中的每个类τ的项t，存在等式x=t∈L2−i，其中x是VJ中的变量;• A是V<$VJ的排列;• ALi对于i= 1， 2，则存在A ∈Li（i= 1， 2）的Ti-模型Ii，使得I1和I2对每个公共排序分配具有相同基数的集合.如果两个I-理论相对于公共类的集合是稳定无限的，那么它们是相容的。但这不是必要条件：许多I-理论不是稳定无限的，而是与某些其他I-理论相容假设T1和T2是相容的不相交的I-理论，使得对于每一种，它们中至少有一个是相容的。然后，如果存在以下情况，则存在用于其并集的语言中的文字集合的满足性判定过程：每个I-理论的语言中的文字集合的可满足性判定过程实际上，如果对于每个安排A，A <$Li对于i= 1或i= 2是不满足的，则在联合中L1<$L2是不满足的理论上，决策程序可以是，第一，计算分离，第二，检查合适的变量集的每一个排列以及分离的每一部分。当且仅当并无发现任何安排令两部分分离均令人满意时，原设定方为不令人满意。给定一组变量V，有与V的分区一样多的排列（至少在一个单排序逻辑中）。 分区的数量，也被称为贝尔数（例如参见[5]），相对于|V|.在实践中，检查每一个安排都是不可行的，即使是对于少量的变量。8.决策程序的一种更实际的方法，合作是通过交换等式（的析取）。9在定理6中，建立排列的变量集大于共享变量集，这通常用于纳尔逊-奥本方法。这对于与非稳定的有限I-理论的结合是必要的，例如，只有有限域的I-理论在[11]中也使用了类似的解决方案，将集合理论与元素理论结合起来，即使最后一个理论不是稳定无限的。组合有限个I-理论的决策过程不仅要求这些I-理论有一个决策过程。 组合中的一些I-理论应该在某些类上是可伸缩的，使得对于组合中的任何两个I-理论，至少有一个对每个（公共）类是可伸缩的。这个要求并不像一阶I-理论那样具有很大的限制性[8]有超过400万个12个变量的排列。[9]这是一个类似于[2]中所提出的正义。44P. Fontaine，P.Gribomont/Electronic Notes in Theoretical Computer Science 125（2005）37在每一种排序上都是不灵活的（定理1.3）。对域基数的要求更严格：要组合在一起的I-理论应该是兼容的。不幸的是，没有简单实用的标准（除了稳定无限性）来确定I-理论是否相容。然而，一些常见的I-理论在相容性方面有很好的性质3空理论语言L中的空的一阶理论定义了I理论，其中每个常数、谓词和函数都是未解释的，并且没有对域施加约束这个I-理论将被称为未解释的它当然是最简单的一个，但它仍然是重要的，因为它允许将未解释的谓词和函数添加到可判定的I-理论的语言未解释的I-理论在组合框架中具有最优行为。经典上，只有它的稳定无限性被利用，因为所有考虑的理论都被假设为稳定无限。然而，它也被注意到，[9]它具有所需的性质，不仅与稳定无限理论相结合，而且与每一个一阶理论相结合。在这里，我们证明了它可以与任何I-理论相结合，无论是否对应于一阶理论。其深层原因可以概括为以下引理：引理3.1设T是多排序语言L中的未解释的I-理论，L是L上的一组文字。如果I=<$D，I <$∈ T是L的一个模型，则存在L的一个模型IJ=<$DJ，IJ <$∈ T，使得对任意类τ和任意J J J基数κ ≥ |Dτ|、|Dτ |= k，且|Dτ J|为|DτJ|对于每个ττ。前面引理的一个推论是不可解释的I-理论的稳定无限性：定理3.2语言L中的未解释的I-理论在L的每一个类集上是稳定无限的。证据 假设L是L中一个满足的有限文字集。存在L的一个解释I= D，I，使得对于L的每一种τ，Dτ是有限的.连续地对每个排序使用引理3.1，可以从I建立一个模型Ij，为每个排序分配基数为0的域。Q因此，未解释的I-理论与每一个稳定无限的I-理论是相容的。但是从引理3.1可以推导出一个更强的结果：定理3.3语言L中的未解释的I-理论与每一个I-理论相容。P. Fontaine，P.Gribomont/Electronic Notes in Theoretical Computer Science 125（2005）37451证据 假设T1是L1语言中未解释的I-理论，T2是L2语言中与L1不相交的任何I-理论。设（L1，L2）和A是一个分离和一个排列，证明了定义2.3的条件。对于L1和L2的每一个共同的排序τ，排列A定义了排序τ的变量的一个划分：两个排序τ的变量在同一个类中当且仅当它们被A的一个模型赋予相同的值。该划分包含给定数量kτ的类。 A Li的模型I i将域Di，τ归于每个公共排序τ，使得|Di，τ|≥kτ。此夕h如果一个nL1是可满足的，那么它有一个模型I 1，该模型I1将定义域D 1，τ赋予每个公共排序τ，使得|D1，τ|= kτ。连续使用引理3.1对每个常见排序，可以构建J从I1一个模型I分配给每个排序相同基数的域解释一2。Q给定语言L中任何可判定的I-理论T，对于结果语言中的文字集，添加任何有限数量的未解释函数、谓词或常数使I-理论保持可判定4数组理论阵列的一阶理论是组合方案中最流行的理论之一。关于它的结果和历史的调查可以在[5，8]中找到。在数组理论的语言中，文字集合的可满足性问题是可判定的。在[8]中，“write”的出现 在[1]证明了叠加演算是（一种）数组理论的一个满足性过程。该理论包含aaa显然有三种可能的排序：索引（i，j）、数组（a，b）和元素（e）。但有些种类可能会合并。 认为数组的排序与元素和索引的排序是不相交的是自然和保守的。10然而，在许多实际情况下，[10]然而，数组理论中的元素可以是数组。但他们的语言应该是不连贯的。例如，读1，写1和读2，写2。46P. Fontaine，P.Gribomont/Electronic Notes in Theoretical Computer Science 125（2005）37合并索引和元素的排序因此，应该考虑两种理论：二分类理论和三分类理论。对应于一阶数组理论的I-理论不像未解释的I-理论那样与每一个I-理论相容。然而，非常积极的结果保持与阵列的I理论的兼容性，这要归功于以下引理：引理4.1设T是L语言中的数组的二排序或三排序I-理论，L是L上的文字集。如果I =<$D，I <$∈ T是L的模型，则存在模型IJ=<$DJ，IJ <$∈ T 使得对于值的排序τ，（或指数）和任何基数κ≥|D|、|DJ|= κ。 如果T 是一个三排序的ττJ JI理论与τ是索引的种类（分别为值），则|Dτ J|为|DτJ|.证据 证据可在附录B中找到。Q稳定无限性是前面引理的直接结果定理4.2L语言中数组的二排序（三排序）I-理论每一个人，都有自己的归宿通常需要使用数组的I理论，元素或索引具有有限域。它的稳定无限性在这些情况下毫无帮助。为了保证仍然可以将数组的I-理论与非稳定无限理论结合起来，还需要在数组排序上不使用不等式。这可以通过在数组语言的分离部分中替换每个不等式t1/=t2来实现，其中t1和t2是数组项read（t1，i）= read（t2，i）其中i是新的索引变量。因此，可能必须在集合VJ中引入新的变量，以验证定理6.定理4.3如果数组的排序不是L的排序，只要在数组排序上不使用不等式，则数组的二排序和三排序I-理论与语言L中的任何I-理论相容。证据 假设T1是L1语言中数组的二排序I-理论，T2是L2语言中与L1不相交的任何I-理论。设（L1，L2）和A是一个分离和一个排列，证明了定义2.3的条件。对于L1和L2的每一个共同的排序τ，排列A定义了排序τ的变量的一个划分：两个排序τ的变量在同一个类中当且仅当它们被A的一个模型赋予相同的值。该划分包含给定数量kτ的类。A L i的模型Ii将域Di，τ归于每个公共排序τ，使得|Di，τ|≥kτ。与空理论相反，它并不直接保证，如果AL1是满意的，那么它P. Fontaine，P.Gribomont/Electronic Notes in Theoretical Computer Science 125（2005）3747J11有一个模型I1（在数组I-theory中），它属于每个公共排序τ a域D1，τ使得|D1，τ|= kτ。考虑两类理论。在L1中使用的公共类τ的每一项都等于在A中使用的一项。设d∈D1，τ不与在A中使用的术语。 我只知道，我的一切，都是一样的，都是一样的。1JD是D1，τ\{d}，并且如果I[read（a，i）] d，则IJ[read（a，i）]=I[read（a，i）]，或者d1，τ11 1否则，其中dJ是DJ的元素一劳永逸地被选中解释J1，τI1仍然是L1中每个文字的模型，也是“读写”公理的模型因为这些公理只是普遍量化的。 如果公式i读作（a，i）=read（b，i）|a=b被IJ对于数组的元素a和bJ1domain inI1，则read（a，i）= read（b，i）for everyi. 可以构建JJ从IJ中分离，使得所有这些元素的仅一个代表被保留。JJ解释I1仍然使“读写”公理和“重写”公理都成立外延性公理假设L1中的数组排序没有使用不等式，IJJ也是L中每个文字的模型。11同样的论点可以应用在三排序的情况下，对于两个ele-sorted。项和指数。因此，如果A ∈L1是T1-satisfable的，则它有一个模型I1∈T1，该模型将每个公共排序τ归结为一个域D1，τ，使得|D1，τ|= kτ。因此，使用引理4.1，可以建立一个模型I1，为每个公共排序分配一个与解释I2具有相同基数的域。Q注意，前面的定理并不意味着如果数组排序是公共排序，那么数组的I-理论是不兼容的。它只是说，如果数组排序是一个常见的排序，那么其他的I-理论必须有一个很好的属性来保证它们是兼容的。例如，数组排序可以是另一个数组I理论的元素排序。此外，数组的I-理论与未解释的I-理论是兼容的，即使两种语言都包含数组的排序。5结论这种新的Nelson-Oppen组合格式在两个方面改进首先，它处理I理论，即，任意的解释，不一定对应于一阶理论。这种改进允许直接处理，例如，线性算术I-理论，算术I-理论，或者I-理论只有无限大小的有限域，例如在验证参数化系统的背景下发布的证明义务中使用。任何具有解释函数和谓词的无量化器的可判定一阶语言都对应于完美描述它的I理论。一个只有无限大小的有限域的I-理论本质上是非线性的。1我48P. Fontaine，P.Gribomont/Electronic Notes in Theoretical Computer Science 125（2005）37稳定地在有限的。本演示文稿的第二个改进是非稳定无限I理论的组合，遵循[9]。多排序框架允许在实践中将非稳定无限的I-理论与对应于空理论的I-理论以及与数组的（I-）理论相至于经典的纳尔逊-奥本框架，这个组合两个I-理论的框架一个组合为两个I-理论的联合提供了一个判定过程，这两个I-理论本身就是一个I-理论。例如，为了处理包含元素列表的数组，对元素排序进行线性运算，列表的I-理论可以与线性运算的I-理论相结合，这要归功于两个I-理论的稳定无限性，并且所获得的I-理论可以与数组的I-理论相结合，使用数组的I-理论的良好行为进行组合。此外，具有函数read1和write1的数组的三排序I理论可以有元素是来自另一个不相交的双排序I-理论的数组对于函数read2和write2，如果唯一的公共排序是第一个I-理论的元素的排序，即，第二个的数组这种组合方案的局限性与严格的多排序框架有关。例如，它不允许考虑元素的列表，这些元素要么是自然的，要么是自然的列表。同样，在定理6中，仍然需要确定可以安全地忽略VJ的所有情况。识别更多具有良好相容性的理论是未来研究的另一个问题我们要感谢匿名评论者的评论。引用[1] A. Armando，S.Ranise和M.Rusinowitch。满足性程序的重写方法信息与计算，183（2）：140[2] S. ConchonandS. 好的。在过程中，强调兼容性。 在P。Narendraan和M. Rusinowitch，编辑，Proceedings of the 9 th International Conference on Tools and Algorithms for theConstruction and Analysis of Systems（Warsaw，Poland），卷2619计算机科学讲义，第537-553页Springer-Verlag，2003年4月。[3] P. Fontaine 和 E. P. Gribomont. 参 数 化 系 统 不 变 式 验 证 的 可 判 定 性 。 在 Proc. Tools andAlgorithms for Construction and Analysis of Systems ， 卷 2619 的 Lecture Notes inComputer Science，第97-112页Springer-Verlag，2003.[4] H.甘青格肖斯塔克灯。以. Voronkov，编辑，自动演绎-Springer-Verlag，2002年7月27日至30日。[5] Z. Manna和C. G.扎尔巴结合决策程序。在十字路口的形式方法：从灵丹妙药到基础支持，计算机科学讲义第2757卷，第381-422页。Springer，2003年。[6] G. Nelson和D. C.奥彭通过合作决策程序简化。ACM Transactions on Programming Languagesand Systems，1（2）：245-257，Oct. 一九七九年P. Fontaine，P.Gribomont/Electronic Notes in Theoretical Computer Science 125（2005）3749[7] D. C.奥彭递归定义的数据结构。Journal of the ACM，27（3）：403[8] A.施通普角W. Barrett，D. L. Dill和J. R.莱维特数组扩张理论的一个判定过程。在第16届IEEE计算机科学逻辑年会（LICS美国电气与电子工程师协会。[9] C. Tinelli和C. G.扎尔巴结合非稳定无限理论。在重症Dahn和L. Vigneron，编辑，第四届一阶定理证明国际研讨会论文集，FTPElsevier Science Publishers，2003.[10] C. Tinelli和C. G.扎尔巴分类逻辑理论的组合决策程序。技术报告04-01，计算机科学系，爱荷华大学，2010年2月。2004年[11] C. G. 扎 尔巴 将 集合 与元 素 组合 。在 N.Dershowitz ，editor ，Verification ：Theory andPractice，volume2772 ofLecture Notes in Computer Science，pages 762-782. Springer，2004.50P. Fontaine，P.Gribomont/Electronic Notes in Theoretical Computer Science 125（2005）37121DJJA定理6的证明条件是必要的。 设I∈ T 成为L的典范。 根据定义，分离时，存在L<$L的模型IJ∈ T。这种解释我J完美定义一个V<$VJ的排列A，而IJ是A <$L2、所以我的A。现在假设解释Ii∈ Ti使得A <$Li为真，其中i= 1， 2。解释Ii定义了在ALi中使用的所有项的划分Ci，使得两个项a和b在同一类中当且仅当IiDa=b。考虑c1∈C1J且c2∈C2，则c1<$c2<$V<$V.但A完美地定义了哪些元素的vvJ都属于同一类。 因此，很容易使分区C和C2在包含相同元素的类上一致设C是项的划分在分区C1和C2中，• 若c1∈C1且c2∈ C2，则c1<$c2∈ C当且仅当c1<$c2非空;• 对每个ci∈Ci，存在c∈ C使得ci<$c。换句话说，Ci的每一个类都完全包含在C的一个类中;• 如果ccJ∈ Ci，且若c，cJ∈ C使得ci<$c且cJ<$cj，则ccJ。我我分区C将允许从I1和I2构建解释I，使得2.第一次约会首先，让我们定义I的域。 对于语言L中的每个排序τ，至少T1或T2是可解的。因此，可以假设I1和I2将相同的域分配给每个公共排序。I自然地为每一个普通的排序分配这个域，而它为每一个只在语言Li中的排序分配由Ii分配的域。其次，对于语言L中的每个排序τ，至少T1或T2是可伸缩的，可以假设I1和I2将相同的元素与V<$VJ中的每个变量相关联。C的每个类c都包含相同种类的元素如果这是两个I-理论的共同排序，则c（V<$VJ）/=，并且对于c中的每一项t，I[t]=I1[t]=I2[t]。 如果不是t，则n个t∈c∈i是一个语言Li，且I[t]=Ii[t]。QB引理4.1的证明首先假设T是三排序的I-理论，τ是值的排序;τJ是指数的排序，σ是数组的排序设m是一个集合，|∆∪Dτ|= κ，J J J并且使得DτJ= Dσ=。解释I解释一：=D，Iis built•τ DτJ=DτJ;1P. Fontaine，P.Gribomont/Electronic Notes in Theoretical Computer Science 125（2005）3751σσ• 对于任何常数a，IJ[a]=I[a];• 对于任何变量x，IJ[x] =I[x];• 如果v∈D，i∈DJ 且a∈D则IJ[read]（a，i）=I[read]（a，i），τ τ σIJ[write]（a，i，v）=I[write]（a，i，v）。这使得IJ成为L的一个模型，但它还没有被完全定义，也不是T的一个模型。 对于Dσ中的每个元素a，DJ\Dσ中有一个元素aJ对应于一个类似于a的数组，但使得有限个元素被替换为a的元素。更正式地说：{write（a，i，v），write（write（a，i，v），iJ，vJ），. . } ∈DJ\DσJ J J对于{v，v，.. . {i，i，. . {\FNMICROSOFTYaHei} 必须特别注意验证可拓性和读写公理。函数当τ是指数的排序时，两种排序的情况和三种排序的情况是相似的。还请注 意 ， 如 果 κ≤κ0 ， |Dτ|≤ 100 ， |DτJ|≤ 100 ， 且 |Dσ| ≤ 100 ， 则 |DJ|≤100%。Qσ0