基于重写的T-决策程序及其条件

理论计算机科学电子笔记174（2007）27-45www.elsevier.com/locate/entcs基于重写的决策过程Maria Paola Bonacina1 Mnacho Echenim2Dipartimento diInformaticaUniversita`degliStudidiVerona Ca摘要基于重写的满足模理论方法包括使用一阶逻辑等式的一般定理证明策略。如果一个人可以证明一个推理系统从一个理论的表示T和一组有限的基本单位子句中生成有限多个子句，那么任何公平的策略基于该系统的可用于T-可满足性过程。 本文介绍了一套充分的条件将基于重写的T -可满足性过程的整个框架推广到基于重写的T -可满足性过程。决策程序。这些条件，统称为subterm-inactivity，将使我们能够获得重写为基础的T-决策程序的几个理论，即那些平等与未解释的功能，数组有或没有扩展和它的两个扩展，有限集与扩展和递归数据结构关键词：重写推理系统，T-决策过程1引言[3]中引入的基于重写的满足性模理论方法在[3，1]中用于设计几种数据结构理论的满足性决策程序，包括数组和记录的理论。这种方法背后的思想是使用基于叠加演算SP的一般定理证明策略，输入集由所考虑的理论的表示组成 T和基础单位子句。由于这样的策略是一阶有效性的半决策过程，如果人们能够证明它们对于任何一组基本单位子句都是终止的，那么它们实际上是T-满足性的决策过程。使基于重写的方法吸引人的另一个特征是，几种理论的组合在概念上变得简单：如果终止被保留，则需要考虑表示的联合。保留终止要求1电子邮件：mariapaola. univr.it2电子邮件地址：echenim@sci.univr.it1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.11.04228M.P. Bonacina，M.Echenim/电子笔记在理论计算机科学174（2007）27表明推理系统是模块化的终止。在[1]中，通过引入变量不活跃的概念，得到了这样一个模态结果：如果组合的理论是变量不活跃的，则基于SP的策略终止于它们的组合，只要它终止于每个单独的理论。就效率而言，与一般的期望相反，通用定理证明器将被更专业的系统（如CVC（[6，15]）或CVC Lite（[4]））超越，[1]的实验结果表明情况并非如此，并且这些程序在几个问题上非常有效。下一步是研究如何将基于重写的方法推广到T-决策问题，或决定无量化器公式的T-满足性当然，在约简为析取范式之后可以应用T-满足性过程，但是这种方法是不实用的。另一种方法是研究如何将基于重写的T-可满足性程序与SAT求解器集成，例如[7，10，2，12，5]中基于同余闭包的T-可满足性程序。在这里，我们选择，而不是研究的问题是否重写为基础的定理证明策略可以自己的T-决策过程。该文件的主要贡献如下：• 我们引入了子项不活跃的概念，并证明了如果理论T是子项不活跃的，则基于公平SP的策略是T-决策问题的决策过程。• 一个理论成为不活跃项所要满足的条件很容易检验，而且除了一个以外，所有的条件都可以自动检验。与[3，1]的终止证明相比，这是一个显著的优势，在[3，1]的终止证明中，人们必须分析可以从表示T和一组基础开始 单位子句此外，我们对SP假设的完全简化序>的唯一要求是，对于每个复合项，t>c t和常数c。• 我们证明了每一个subterm-inactive理论也是variable-inactive理论。• 我们表明，在[3，1]中考虑的几个理论，以及阵列理论的两个扩展，是subterm-不活跃的。由于篇幅所限，大部分的证明都不能包含在本文中。他们都可以在[8]中找到。2预赛2.1术语、文字和子句给定一个签名n，n表示n中具有元数n的函数的集合。因此，0表示中的常数集。我们考虑的标准定义的术语，字母和字母的条款。像往常一样，子句被假设为变量不相交的。在以下，是无序相等，Da是或/。字母l r u v和t将表示项、w、x、y、z变量，并且所有其它小写字母将表示常数或函数符号。 给定一个项t，top（t）是如下所M.P. Bonacina，M.Echenim/电子笔记在理论计算机科学174（2007）2729t我们还将考虑Var对文字和子句的自然扩展：例如，如果C是子句，则Var（C）是出现在C中的变量的集合。给定一个理论的表示T，如果一个函数符号出现在T的公理中，它就被解释，否则就不被解释。T-可满足性问题是判定一组基本单位子句在T中是否可满足的问题。更一般的T-判定问题是判定T中任何基公式的满足性的问题。在不失一般性的情况下，我们可以假设所考虑的基础公式是子句的合取定义2.1给定一个签名f，选择函数是一个从f到N的函数，使得对于所有f∈ f，Γ（f）∈ {1，.，arity（f）}。Ω表示Ω的选择函数集。选择函数选择一个项中的参数例如，对于函数符号f和选择函数Γ，如果Γ（f）= i，则Γ从项f（t1，. ，tn）。名称“选择函数”也用于选择子句中的文字的函数：这两个定义是兼容的，因为这样的我们定义了无符号的概念，它防止某些功能或常量符号出现在子句中。定义2.2（无符号性）给定一个项t，Φ（t）表示出现在t中的函数和常数符号的集合。此外，令Φ（lD a r）= Φ（l）<$Φ（r），Φ（C）=L∈C Φ（L）。给定一组函数和常数符号，则项t为J-symbol-free，如果Φ（t）一个文字（resp.子句）是无符号的，如果出现在其中的每个项都是。如果C语言中包含函数符号的每个文字都是严格无符号的，则子句是无符号的2.2扁平化如果项t是常数或变量，则t的深度是深度（t）= 0，否则深度（f（t1，.，tn））= 1+ max {深度（ti）|i = 1，.，n}。lD a r的深度是max（depth（l），depth（r））。如果depth（l）+depth（r）≤1，则正字面值为pixalat，如果其深度为0，则负字面值为pixalat定义2.3如果深度为0，则字面量是严格可解的。对于子句C，令Maxd（C）= max{depth（t）|t是出现在C中的项。如果子句C的所有字面值都是，则子句C是严格的，重新的，严格的我们将大量使用人工智能。转换的操作在于将签名上的基础子句S的有限集合转换为签名上的基础子句Sj的有限集合，以这样的方式：•J是通过将有限个常数加到•SJ中的每个非单位子句都是严格可拓的，30M.P. Bonacina，M.Echenim/电子笔记在理论计算机科学174（2007）27叠加调解法反射方程式分解Cl[uJ]rDut（C<$D<$l[t]r）σCl[uJ]/rDut（C<$D<$l[t]/r）σ C<$uJ/uCσ楚 tuJtJ（Ct/tJutJ）σ㈠、 ㈡、 ㈢、㈣(i) 、㈡、 ㈢、㈣（五）当notationl[uJ]m表示uJ在l中作为subterm时，σ是u和uJ的最大基因均衡(i) ：uσ/≤tσ;(ii) ：L∈D：（ut）σ/≤ Lσ;(iii) ：l[uJ]σ/≤rσ;(iv) ：<$L∈C：（l[uJ]dar）σ/≤Lσ;(v) ：<$L∈C：（uJu）σ/μLσ;(vi) ：L∈ {uJtJ}C：（ut）σ/μ Lσ。Fig. 1. SP的扩展推理规则：在扩展规则中，推理线以下的内容被添加到包含推理线以上内容的子句集合中。•SJ中的每个单位子句都是可替换的，• 对于所有的集合T，T ∈S和T ∈SJ都是等价的。这个附加操作相当简单，并且比[ 3 ]中的操作更一般，在[3]中只考虑单位子句。作为一个例子，考虑集合S={f（f（a））b<$f（c）/d}：通过引入新的常数c1，c2和c3，我们得到了等价集SJ={f（a） c1，f（c1） c2，f（c）c3，c2b/c3/d}。2.3基于重写的推理系统简单化序>是一个稳定的、单调的、包含子项序的序：如果s>t，那么对于任何上下文c和替换σ，c[s]σ>c[t]σ，如果t是s的子项，那么s>t。完全单纯化序（completesimplification ordering，简称CSO）是一种在基项上为全的单纯化序。如果s>t，我们就写ts。有关订购的更多详细信息，请参见，例如，在[11]中。在下文中，除非另有说明，否则我们将假设对于所考虑的CSO，如果t是复合项并且c是常数，则t>c。这种情况是部分M.P. Bonacina，M.Echenim/电子笔记在理论计算机科学174（2007）2731C D严格包容D>·CCC[u]lr简化u=lσ，lσ>rσ，C[u]>（lr）σC[rσ]lrCtt删除当reD>· C如果D≥· C和C≥/· D;ndD≥· CifCσD（asmulti s ets）fors om e sutitionσ。在实践中，理论方法适用于所有变量的合并：如果D≥· C和C≥· D、保留最老的条款。图二. SP的收缩推理规则：在收缩规则中，双推理线以上的内容从子句集中删除，双推理线以下的内容添加到子句集中。[1]中考虑的所有理论的T-优性要求我们把这个要求简单地称为善良要求。叠加演算，或SP（见[13]），是一个基于重写的推理系统，它对于一阶逻辑是反驳完全的。它由扩展规则（见图1）和压缩规则（见图2）组成，并且基于以标准方式扩展到文字和子句的术语的CSO给定一个CSO>，我们写SP>为SP配备>。子句C相对于子句集合S中的SP是冗余的，如果S可以通过应用从S{C}导出SP中的收缩规则。 由于SP是本文中唯一的推理系统，因此我们将关于SP的冗余写为冗余。一个推论在S中是冗余的，如果它的结论或它的前提之一在S中是冗余的。SP-策略由SP连同控制推理规则的应用的搜索计划一起给出。SP>-推导是一个序列S 0系列> S 1系列 ...联系我们 ... 、其中每个Si是子句的集合，通过对Si−1中的子句应用扩展或压缩规则而获得。这种派生的限制是持久化子句的集合：S∞=j≥0i≥jS岛一个派生词S0SP>. SnSP>. 是公平的，如果所有的扩展推理在SP>与S∞的前提是多余的，在一些Sj，j≥0。 一个搜索计划是公平的，如果它控制的所有派生都是公平的，而一个SP>-策略是如果它的搜索计划是公平的。一个子句集S是饱和的，如果通过SP-推理从S中的子句生成的每个子句都是冗余的。一个子句C对于>是可变无效的（见[1]），如果C中没有一个极大文字是等式x，其中x∈/Var（t）. 一个类的设置是可变的-对于所有32M.P. Bonacina，M.Echenim/电子笔记在理论计算机科学174（2007）27它的子句对于>是变量无效的。表示T对于>是可变无效的，如果从S0=T <$S导出的公平SP>的极限S∞是可变无效的。 当没有混淆是可能的，我们会说，一个条款（分别。一组子句或一个理论演示）是可变的-非活动的，没有任何提及>。我们用深度保持的概念来总结这些概念。直观地说，这个概念可以防止扩展推理规则生成的子句变得任意大。定义2.4设C，CJ和D是子句，并假设D是通过一元推理从C生成的：如果Maxd（D）≤Maxd（C），则该推理是深度保持的假设D是由C和CJ通过二进制推断生成的：如果Maxd（D）≤max{ Maxd（C），Maxd（CJ）}，则该推断是深度保持的。3子项不活动性叠加演算终止于不同理论的可满足性问题的证明是基于对可以由推论生成的子句种类的枚举（见[3，1，8]）。然而，S∞中的子句数可以n2它是指数级大的（例如，它可以包含理论中的O（2关于数组，详见[1]），一般来说，这样的证明包括表明所有生成的子句属于几个类别之一：如果这些类别中的每一个都包含有限个子句，那么S∞也将包含有限个子句。 这些证明可以很长，在每一个新的推论中，都可能产生一个要处理的新的范畴。 本节我们引入一组条件，保证基于SP>的公平策略是所考虑理论的决策过程。这些条件很容易验证，更重要的是，几乎所有条件都可以自动验证。非正式地，我们将考虑T-决策问题，其子句可以分为三个不相交的集合：• 一组Tg的基本从句，• - 非基础子句的集合T1，其表示可以通过考虑一个解释的函数符号而推导出的属性，• 一组T2的非基础子句，表示两个被解释的函数符号在T中可能相互作用的方式。这种模式适用于T-决策问题的几个理论的利益，如，例如，理论的数组。例3.1数组A的理论，基于签名A={ select， store}，其中select的arity为2，store的arity为3，公理化如下：x，z，v select（store（x，z，v），z） 第五章（一）x，z，w，v. （zw）select（store（x，z，v），w）select（x，w））.（二）具有可拓性Ae的数组理论由公理（1）和（2）以及以下可拓性公理定义：1996年，（z. select（x，z）select（y，z）select（y，z）（三）M.P. Bonacina，M.Echenim/电子笔记在理论计算机科学174（2007）2733理论Ae的基于重写的T-判定过程将基础子句的集合Tg连同{（1），（2），（3）}作为输入。这个集合本身可以分解为两个不相交的子集：T2={（1），（2）}，它描述了选择和存储交互的方式，T1={（3）}，它描述了可以从选择函数推导出的相等属性。当然，这些集合可以相互作用，并且有必要尽可能地控制这些相互作用以保证终止。在给出任何正式的定义之前，我们非正式地列举了这些集合应该满足的要求以及满足这些要求的条件常规属性(i)T2中的每个子句表示当组合至多两个解释的函数符号时验证的单个性质，并且T1中的每个子句表示可以通过考虑单个解释的函数符号（闭包）来推导的性质;(ii) 任何生成持久化子句的SP>-推理都是深度保持的（可扩展性）。二元推理(i)T2中的一个小句和T1中的一个小句之间不存在二元SP>（interaction-freeness）;(ii)T1→T2中的小句和Tg中的小句之间的二元SP>-推理生成T1或Tg中的小句（闭包+负断开）;(iii)T2中两个小句之间的二元SP>-推理生成一个小句，该小句最终被删除（饱和）;(iv)T1中两个子句之间的二元SP>-推理生成T1中的子句或在Tg（闭合）中。一元推论(i)T2中的一元推理生成最终被删除的小句（饱和）;(ii)T1中的一元推理生成一个在T1中、在Tg中或最终被删除的子句（变量不活动保留）。在下面的小节中，我们正式定义这些概念。3.1对T2的我们把T2上的条件统称为饱和闭包.一般来说，这些条件确保T2是饱和的，并且由涉及T2中的子句的二元推理生成的每个子句都在T1或Tg中。定义3.2（有序可达性）一个子句C是有序可达的，如果它只包含严格可达的文字，除了一个，比如lD a r。此外，它必须是rl，并且r必须只包含出现在l中的函数符号。例3.3考虑以下条款：34M.P. Bonacina，M.Echenim/电子笔记在理论计算机科学174（2007）27C=f（a）b<$c/d，CJ= f（g（a））g（a）<$c/d。这两个条款是并列的。定义3.4（内部闭包）设S是子句集合，Γ是选择函数。S是Γ-内闭的，如果对每个子句C∈S和C中每个非严格的字面量L=lD a r：• 如果L为负数，则：icn.1：对于l的每个深度为1的子项u，Var（C）≠Var（u），icn.2：S的子句中的每个正文字是Φ（L）-无符号的。• 如果L是正的，那么我们必须有rl，并且：icp.1：深度（l）= 2，且l包含深度1的唯一子项u，icp.2：Var（C）=Var（l），icp.3：如果top（r）= top（l），则深度（r）= 0且Var（C）=Var（u），IC山口4：如果top（r）=top（l），则thendepth（r）=l，r|qf=l|qf，l|qfapearsnwheeelsenlorr，并且Var（l）\Var（u）={l|qf}。还通过强制T2是饱和的，并且出现在T2中的每个包含常数的文字都是严格可忽略的（形式上，每个子句都不受子符号的限制），我们得到以下饱和闭包的定义：定义3.5（饱和-闭）设Γ∈Ω，一个子句集S是Γ- 饱和-闭的，如果• 它是饱和的，• S中的每一子句都是不含子符号的，• S中的每一子句都是有序的，• S是Γ-内闭的。3.2对T1的限制对T1施加的限制阻止了它的子句与T2的交互，并控制了涉及这些子句的推理所生成的子句定义3.6（弱可拓性）一个子句C是弱可拓的，如果C只包含深度项至多为1的文字，并且至少有一个非严格可拓的非基文字lD a r。此外，如果C包含文字xD a t，则t的深度为0。例3.7子句C=f（a） b∈f（x）/d是弱对称的。定义3.8（变量不活动保持）给定一个函数Γ∈Ω，子句C是Γ-变量不活动保持的当且仅当：vip-1：对每个变量x∈Var（C）和C中的每个非严格可达的文字L，x是L中深度为1的项的变量。M.P. Bonacina，M.Echenim/电子笔记在理论计算机科学174（2007）2735vip-2：如果C包含负文字l/r，其中top（l）= top（r）= f，则C也包含文字xt，使得t是变量且Var（C）={x，t}，或Var（C）={x}。对于这个例子，设qf=Γ（f），则：a. 如果t是可变的，则n{x，t}={1|qf，r|qf}，b. 如果t是常数，则存在常数c（不一定等于t），使得t {x，c}={l|qf，r|qf}。一个子句集S是保持Γ-变元不活动的，如果S中的每个子句都是。例3.9令I={Inj}，其中Inj是元数为1的谓词，考虑基于签名AI的理论AI，它由例3.1的公理（1）和（2）公理化，下面的公理表示为（inj）：Inj（x）Inj（x）Inj（x） （z/w = select（x，z）/select（x，w））。直观地说，谓词Inj对于数组a为真，当且仅当a中的所有元素都是两两不同的（a是单射的）。考虑以下子句形式，逻辑上等同于Inj（a）：C = zw= select（a，z）/select（a，w）。这个子句包含一个不是严格意义上的文本，L= select（a，z）/select（a，w）。我们有Var（C）={z，w}，这两个变量以L中深度1的形式出现。 设Γ是Ω中的任意函数，使得Γ（select）= 2。 由于zW在C中也是一个字面量，并且条件（vip.2.a）在C上成立，这个子句是Γ-变量-非活动保留的。定义3.10（外闭包）设C是子句，SJ是子句集，Γ∈Ωf，且f∈Ω，letqf=Γ（f）. 对于C中的每一个正文字lr，C是r-externalycloseedfromromSJif，使得top（l）=f，EC.1：top（l）= top（r），ec.2：C中的所有其他文字都是严格可重写的，ec.3：l|qf=r|Q是唯一在C中可变的，并且它在L或R中的其他情况下是可变的。EC.4：SJ的子句中的每个负文字都是{f}-符号自由的。一个子句集S是从Sj Γ-外闭的，如果S中的每个子句都是。例3.11设S={ Swap}，其中Swap是元数为4的谓词，考虑基于签名S的理论AS，并由（1），（2）（A的公理，见例3.1）和以下公理（swp）表示Swap（x，y，z1，z2）优惠选择（x，z1）选择（y，z2）select（x，z2）select（y，z1）好吧（w/z1w/z2select（x，w） select（y，w））。给定常数b，bJ，i和iJ，原子Swap（b，bJ，i，iJ）为真当且仅当bJ与b相同，除了索引i和iJ处的元素被交换。考虑该条款D=wiwij select（b，w） 选择（bJ，w）。36M.P. Bonacina，M.Echenim/电子笔记在理论计算机科学174（2007）27设Γ是Ω中的任意函数，使得Γ（select）= 2，设SJ={（1），（2）}.很容易检验D满足条件（ec.1）到（ec.4），因此从SJ是Γ-外闭的。定义3.12（免疫性）给定两组子句S和SJ以及函数Γ∈Ω，S对SJ是Γ-免疫的当且仅当• S中的每个子句都是弱可解的，• S中的每个子句都是Γ-变量非活动保持的，• S是从Sj的Γ-外闭的。定义3.13（无相互作用性）给定两组子句S和SJ以及一个函数Γ∈Ω，如果满足以下条件，则S是与Sj无Γ -相互作用的：letfbafunctionsymbol，letpf=Γ（f），并且suppsethat，• 或者f同时出现在S中的子句的正字面量和SJ中的子句的字面量中，• 或者f同时出现在SJ中的一个子句的肯定字面量和S中的一个子句的字面量中。那么对于所有子句C∈S<$SJ包含文字L=lD a r，使得f出现在l或r中，以下条件必须成立：如果f仅作为L或R的顶部符号出现，if. 2：ifC ∈S，|pf是一个字符串，并且如果该字符串不可用，则|pfisa const，如果C ∈SJ且L是整数，则|pf是depth1的一种形式，if. 4：ifC ∈SJ且L为p〇sitive，nu=l|pfisa termofdepth1，并且difr是不可用的，|pf是在Var（u）中可变量化的变量。例3.14考虑S={D}，其中D是例3.11的子句，SJ={（1），（2）}。这些集合的唯一共同功能符号是select。 设Γ是Ω中的任意函数，使得Γ（select）= 1。那么很明显，D满足条件（if.1）和（if.2），并且SJ中的子句满足条件（if.4）。因此，S是与SJ无Γ-相互作用的。类似地，考虑例3.9中的子句C，则{C}也与SJ无Γ-相互作用。3.3对Tg的限制最后，我们定义了Tg的不连通性的概念。定义3.15（正可达性）一个子句C是正可达的，如果每次C包含一个不严格可达的正文字，这个文字是可达的，并且C中的所有其他文字都是严格可达的。例3.16考虑以下子句：M.P. Bonacina，M.Echenim/电子笔记在理论计算机科学174（2007）2737C=f（a）b<$c/d，CJ=f（f（a））/b<$f（c）/d，条款C和CJ都是肯定的。定义3.17（负断开）设C是子句，SJ是子句的集合。C与SJ是负不连通的，如果只要C包含负文字l/r使得深度（l）≥2，则SJ中子句的每个正文字都是Φ（C）-无符号的。一个子句集S与SJ是负不连通的，如果S中的每个子句都与SJ是负不连通的。定义3.18（平面不连通）给定一个子句C和一组子句SJ，C是SJ的非连通不连通的，当且仅当C• 积极地，• 与SJ负断开。一个子句集S是与Sj不连通的，如果S中的每个子句都是。例3.19任何一组附加的基础子句都是与任何其他子句Sj的集合分离的。事实上，这样的集合是平凡正可解的;因为它的所有负文字都是严格可解的，所以不存在深度（l）≥2的文字l/r，并且集合也与SJ负不连通。3.4子项不活动性我们介绍了基本概念的subterm不活动，这保证了SP的终止在所考虑的理论的决策问题定义3.20（子项不活动性）设Tg，T1和T2是三个不相交的子句集。如果在Ωk中存在两个函数Γ和ΓJ使得：• Tg只包含基础子句，并且与T1<$T2不连通，• T1与T2是Γ免疫的和ΓJ无相互作用的，•T2是Γ-饱和闭的.如果存在一个划分TgT1T2，则理论T的表示是无子项的的T 使得T1，T2，T3，T4，T5，T6，T7，T8，T9，T10，T11，T12，T13，T14，T16，T17，T18，T19由于我们可以将任何一组基础从句添加到子项非主动陈述中，因此我们可以安全地将其添加到子项非主动陈述中：命题3.21如果T是一个subterm-inactive表示，则对于每一组基础子句S，存在一组基础子句SJ，使得Sj<$T等价于Sj <$T，并且SJ <$T是subterm-inactive的。在下面的章节中，我们将给出几个不动隐式项理论的例子。在此之前，我们陈述我们在subterm-inactivity假设下获得的主要结果：38M.P. Bonacina，M.Echenim/电子笔记在理论计算机科学174（2007）27定理3.22给定一组子句T=TgT1T2，使得TgT1，T2T2是一个子项无效元组：(i) 如果D是由T中的 SP-推断生成的持久子句，则推断是深度保持的，并且：• 或者D接地，并且T1、T2、T3、T4、T5、T6、T7、T8、T9、T10、T11、T12、T13、T14、T16、T18、T19、T1• 或D不接地，且T1、T2、T3、T4、T5、T6、T7、T8、T9、T10、T11、T12、T13、T14、T16、T17、T18、T19(ii) 公平SP>-策略是T.(iii) T是不活跃的变量。定理3.22的证明，特别是（i）的证明，需要考虑所有可能的推论，这些推论可以应用于集合Tg，T1和T2。不同情况的完整处理和其他证据都可以在[8]中找到4数组理论的变体在下面，我们考虑数组理论（见例3.1）及其两个扩展。在[3]中表明，Ae中的满足性问题可以归结为A中的等价满足性问题，并且叠加演算给出了A的一个满足性过程：极限S∞是有限的证明可以在[1]中找到。这种分析需要很长的证明：对于A，S∞中的子句可以属于14类子句中的任何一类我们得到以下结果：定理4.1 A的表示是无子项的。证据 我们证明了元组，，{（1），（2）}是subterm-inactive的。• 可以应用于{（1），（2）}的唯一推论是（1）和（2）之间的叠加。这将生成子句zzselect（x，z）v，该子句将被删除。 因此，该集合是饱和的。• 检查{（1），（2）}中的子句是否有序是很简单的。由于它们不包含任何常量，因此它们也不包含子符号。• （1）和（2）中的最大文字都是正的，可以检查{（1），（2）}是Γ-内闭的，对于任意选择函数Γ使得Γ（select）= 2。Q因此，通过定理3.22（ii），我们推导出：推论4.2任何公平的SP>-策略都是具有或不具有可拓性的阵列理论的决策过程.4.1内射谓词接下来，我们考虑用内射谓词扩充的数组理论AI，如例3.9所定义：Inj（x）Inj（x）Inj（x） （z/w = select（x，z）/select（x，w））。M.P. Bonacina，M.Echenim/电子笔记在理论计算机科学174（2007）2739一一一一我们假设内射谓词的每一次出现都有一个常量作为参数。在这一假设下并没有丧失一般性。例如，子句Inj（f（a））B可以安全地替换为子句Inj（b）B和常量f（a）b，其中b是一个新常量。 仍然不失一般性，我们可以假设，如果内射性谓词出现在非单位子句中，则该子句的形式为Inj（a）<$p或<$Inj（a）<$p，其中p是命题变量。事实上，这样的公式可以从S通过重复替换形式Inj（a）D（resp.<$Inj（a）<$D），其中D不是命题变量，由子句Inj（a）<$<$pa和pa <$D（分别为<$Inj（a）<$$>paandpa<$D），其中pa是一个新的命题变量。这样得到的公式等价于S（详见[14]）。我们用下面的方法删除所有出现的谓词Inj。对于每个常数a，我们考虑子句Ca及其否定形式CJ，分别定义为通过：Ca=zw select（a，z）/select（a，w），CJ=（sk1/sk2）select（a，sk1）select（a，sk2）），其中sk1和sk2是新的Skolem常数。注意，根据定义，Inj（a）在逻辑上等价于n，z，w。（z/w<$select（a，z）/select（a，w）），Ca是后一个公式的子句形式。因此，Ca和Inj（a）在逻辑上是等价的;类似地，CJ和<$Inj（a）在逻辑上也是等价的。因此，我们可以安全地用Cap代替Inj（a）p形式的每个分句，用CJp的小句形式代替<$Inj（a）p形式的每个分句。例4.3令S={<$ Inj（a）<$Inj（b）}。通过引入新的命题变量pa，我们得到集合SJ={<$ Inj（a）<$$>pa，Inj（b）<$pa}，经过上述变换，我们得到SJJ={sk1/sk2pa，select（a，sk1）select（a，sk2）选择a，zw{select（b，z）/select（b，w）}其中z和w是隐式泛量化变量。给定一个子句集S，由此得到的子句的约简集可等价于S，我们有：引理4.4设{a1，.，an}是一组常数，对于所有i∈ {1，.，n}设pi是一个命题变量（或命题变量的否定），并定义Ci= λz，w. zwselect（ai，z）/select（ai，w）.理论A <${Ci<$pi|i = 1，. ，n}是子项不活动的。证据我们证明了元组{C1}p1，.，Cn<$pn}，{（1），（2）} n是子项非活动的。在定理4.1中，我们证明了{（1），（2）}是Γ-饱和闭的，其中Γ（select）= 2。考虑任意函数ΓJ∈Ω，使得ΓJ（select）= 1，且a40M.P. Bonacina，M.Echenim/电子笔记在理论计算机科学174（2007）27GGGGG第C这一子句对{（1），（2）}是Γ-免疫的：我们已经在例3.9中证明了Ci是Γ-变量非活动保持的，并且很容易验证Cipi也是从{（1），（2）} Γ-外部封闭的;其他条件验证起来很简单。它也是来自{（1），（2）}的ΓJ-无相互作用的，因此结果是。由于这些条件对于形式C i p i的每个子句都是满足的，很明显，{C1 p1，. ，Cn<$pn}，{（1），（2）}<$是无子项的，证明是完备的.Q因此，通过定理3.22（ii），可以使用SP>-策略连同公平搜索计划来测试A {Cip i}的可满足性。|i = 1，.，n}。 因此，我们得到以下结果：推论4.5公平SP>-策略是AI的决策过程.4.2Swap谓词我们现在转向用交换谓词扩充的数组的理论AS，如例3.11中所定义：Swap（x，y，z1，z2）优惠选择（x，z1）选择（y，z2）select（x，z2）select（y，z1）好吧（w/z1w/z2select（x，w） select（y，w））。考虑一个基AS-公式S.类似于内射谓词的情况，直到将替换等式添加到S，我们假设交换谓词的每次出现仅具有常数作为自变量，并且该谓词出现的子句具有Swap（b，bJ，i，iJ）替换<$p或<$Swap（b，bJ，i，iJ）替换<$p的形式。我们以如下方式移除谓词Swap的所有出现：对于每个常量元组G=b，bJ，i，ij，其中b和bJ是排序数组，i和iJ是考虑了Dj的公式DG及其否定形式DJ分别定义如下：DG= select（b，i）select（bJ，iJ）select（b，iJ）好吧 （w/i w/iJselect（b，w）select（bJ，w））J= select（b，i）/select（bJ，iJ）select（b，iJ）/select（bJ，i）（sk/i_sk/i_J_select（b，sk）/select（b_J，sk）），其中sk是新的Skolem常数。根据定义，Swap（b，bJ，i，iJ）和DG是log-等价，并且可以检查<$Swap（b，bJ，i，iJ）和DJ也是合乎逻辑的相当于给定一个元组G=Bb，bJ，i，iJ，我们因此可以安全地用DGp的子句形式替换Swap（b，bJ，i，iJ）p形式的每个公式，形式p与DJ的从句形式好吧 我们得到等于S。在下面的引理中，从句Dk来自从句DG的小句形式;DG的小句形式的其余部分是基础，大卫琼斯：他们不需要证明不作为。DM.P. Bonacina，M.Echenim/电子笔记在理论计算机科学174（2007）2741KKK引理4.6令{bk，bJ，ik，iJ|k = 1，.，m}是一组常数，并且对于每个K Kk∈ {1，. ，m}，设pk是命题变量（或命题变量的否定），变量）并考虑子句Dk= wikwij select（bk，w）select（bJ，w）.理论A <${Dk<$pk|k = 1，.，m}是子项无效的。证据 我们证明了，{D1<$p1，. ，Dmpm}，{（1），（2）}是子项不活跃的。很容易检查{（1），（2）}是Γ-饱和闭的，其中Γ（select）= 2。考虑一个子句Dk，应用定义3.12可以看出，Dkpk对{（1），（2）}是Γ-免疫的（也见例3.11）。如例3.14所示，Dk为ΓJ-对于任意的ΓJ，使得ΓJ（select）= 1，{（1），（2）}是无相互作用的，并且它是简单的证明了Dk∈pk也是从{（1），（2）}中ΓJ-无相互作用的。 因此，对于每个k，⟨∅,{Dk∨ pk},{(1),(2)}⟩ is subterm-inactive. 因为这对每个k都是真的，所以我们有结果。Q对于推论4.5，我们可以推导出：定理4.7公平SP>-策略是A S的一个决策过程.最后，考虑由（1），（2），（inj）和（swp）公理化的理论Aj，设Γ和ΓJ是选择函数，使得Γ（select）= 2和ΓJ（select）= 1。给定集合A ={Ci<$pi|i =1，. ，n}且B ={Dk<$pJ|k = 1，. ，m}，对于上面定义的选择函数Γ和ΓJ• 根据引理4.4，A，{（1），（2）} A是子项不活跃的，• 由引理4.6可知，B，{（1），（2）} B是子项不活跃的。我们推断元组AB，{（1），（2）}也是subterm-inactive的。因此，我们得到以下结果：定理4.8公平SP>-策略是A j的一个决策过程.4.3一个不明显的例子下一个例子表明，尽管元组成为subterm-inactive所需的条件非常强，但其中一些条件很严格，并允许我们指出一些不明显的结果。例4.9考虑下面的谓词：Const y（x）惠z。select（x，z）y，它表示数组表示常量函数的属性。 很容易为了检查给定的两个常数a和e，T=A { Conste（a）}不是子项-非活动的：不存在使得Conste（a）对任何其他集合是Γ-免疫的（条件（ec.1）不成立），或者是Γ-饱和闭的（条件（icp.1）不成立）。实际上，T甚至不是变量无效的;考虑下面的集合：S={ store（a，i，e1）aJ，Conste（a），ConsteJ（aJ）}，42M.P. Bonacina，M.Echenim/电子笔记在理论计算机科学174（2007）27优惠{store（a，i，e1）aJ，select（a，z）e，选择（aJ，z）eJ}。M.P. Bonacina，M.Echenim/电子笔记在理论计算机科学174（2007）2743单元子句store（a，i，e1）的叠加aJ到公理zwselect（store（x，z，v），w）select（x，w）产生子句W iselect（a，w）select（aJ，w）.（4）通过select（aJ，z）简化该子句eJ和select（a，z）e产生子句wieeJ.此子句不是可变非活动子句，因为它不能被删除，S∞也不是可变-无效的5决策过程基于子项不活动性的方法使我们能够重新获得SP在T-可满足性问题上的其他终止结果，并将它们推广到T-决策问题.5.1有无外延的有限集有限集合理论是基于签名集合={ member， insert}，其中member和insert都有2元。直观地说，member（e，s）是true，如果e是s的元素，insert（e，s）将元素e插入集合s。该理论由以下表述定义，用FS表示：阿 克 斯 河 谷 m e m b e r（ v ， insert （ v ， x ） ） true ，（5）1999年，第五，第五。v/w= member（v，insert（w，x））member（v，x）.（六）具有外延性的有限集理论由FSe提出，它由公理（5）和（6）以及以下外延性公理组成：1996年，（同上）（成员（v，x）member（v，y）） y.（七）文[3，定理8.1]证明了任何FSe-决策问题都可