集合论中的限制量化和有限枚举的可满足性问题研究 - 2016年电子笔记322 - 意大利卡塔尼亚大学

0000可在www.sciencedirect.com在线获取理论计算机科学电子笔记322（2016）69-86www.elsevier.com/locate/entcs集合论中具有限制量化和有限计数的Domenico Cantone1 Marianna Nicolosi-Asmundo2部意大利卡塔尼亚大学数学与计算机科学系摘要我们解决了集合论的三个排序片段（表示为3LQSTR）的满足性问题，允许对单个和集合变量的量化的限制形式以及有限枚举运算符{-，-，.. .，-} 在单个变量上，通过显示它享有小的模型属性，即，任何3LQSTR的令人满意的公式具有有限模型，其大小仅取决于公式本身的长度。几个集合论构造可以用3LQSTR-公式表示，例如幂集合运算符和无序笛卡尔积。特别是，关于后一个结构，我们表明，当有限枚举是允许的，所得到的公式是指数短于在他们的情况下。保留字：满足性问题，集合论，限制量化，有限枚举。1引言可计算集合论研究集合论公式（也称为三段论）的特定集合的可判定性问题。到2001年为止，可计算集合论的主要结果已经收集在[7，13]中。我们还提到，集合论片段的最有效的判定过程构成了证明验证者AlfantnaNova[17]的推理核心本文给出了集合论语言3LQSTR（具有有限枚举和限制量化器的三层量化三段论）的可满足性问题的可判定性结果，3LQST R是一个涉及个体变量、集合变量和集合变量的三种排序的量化音节，范围这项工作得到了波兰国家科学中心研究项目DEC- 2011/02/A/HS 1/00395的部分支持。1电子邮件：cantone@dmi.unict.it2 电子邮件地址：nicolosi@dmi.unict.ithttp://dx.doi.org/10.1016/j.entcs.2016.03.0061571-0661/© 2016作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。70D. Cantone，M.Nicolosi-Asmundo/Electronic Notes in Theoretical Computer Science 322（2016）690000000000在一个给定的非空的宇宙D的元素，D的子集，和集合的子集D，分别。3LQSTR的语言允许谓词符号=和∈以及对个体和集合变量的量化的限制形式。语言3LQST R扩展了[ 9 ]中提出的3LQS R，因为它允许有限枚举运算符{-，-，.，-}对单个变量。尽管它的简单性，3LQSTR允许一个表达集合论的几个结构其中，最全面的一个是集前，这反过来又允许一个表示其他集理论的运营商，如一些变种的权力集和无序笛卡尔积。关于后者，我们将看到它可以用线性长度的3LQSTR-公式表示。另一方面，如果去掉有限计数算子，则需要指数长的3LQSR-公式来表示它。证明是通过展示如何从满足3LQSTR-公式的给定模型中提取出另一个有界有限的非线性基数本文的结构如下。在第2节中，我们介绍了可计算集合论中关于多排序分层三段论的一些相关工作。然后，在第3节中，我们首先介绍一种更通用的语言的语法和语义，表示为3LQST0，然后提供一个可判定的语义限制来描述我们感兴趣的片段3LQSTR。随后，在第4节中，我们证明了几个集合论结构可以很容易地用3LQSTR-公式表示。在第5节中，提供了证明我们的主要可判定性结果所需的机器，在第6节中，概述了3LQSTR的小模型性质，从而解决了3LQSTR的可满足性问题。然后，在第7节中，我们给出了无序笛卡尔积的两种不同表示。第一个，使用有限枚举算子，在乘积的长度上是线性的，第二个，不涉及有限枚举算子，是指数增长的。最后，在第8节中，我们得出了结论。2相关工作在可计算集合论中建立的大多数可判定性结果都涉及单排序的多级三段论，即只涉及一种类型变量的公式集合，范围遍及冯·诺依曼集合论域。另一方面，很少有可判定性结果已被证明为多排序分层三段论，admitting几种类型的变量。尽管在计算机科学和数学的许多领域中，人们经常处理多排序语言。两级三段论语言（2LS）的可满足性的一个有效的判定过程，一个允许两种变量（对于个体和对于个体集合）的片段，基本的集合论运算符，例如，[15]中已经提出了∈三种排序语言3LSSPU（具有单例、幂集和一般联合的三级三段论），除了2LS中已有的运算符和谓词外，还允许三种类型的变量，以及单例、幂集和一般联合运算符，D. Cantone，M.Nicolosi-Asmundo/Electronic Notes in Theoretical Computer Science 322（2016）6971000在[4]中被证明是可判定的最近，在[9]中，涉及三种变量的三层量化三段论3LQSR已被证明具有可判定的可满足3LQSR的判定算法受[4]中提出的证明3LSSPU可判定性的过程的启发。特别是，[9]中引入的相对化解释的概念可以被看作是[4]中定义的小模型赋值概念的变体。语言3LQSR，以及它的扩展3LQSTR在本文中介绍，不允许一个表示一般的联盟的结构。另一方面，后一个构造是3LSSPU的原始运算符。后来，在[10]中，4LQSR，一个允许四种变量的四级量化音节的满足性问题，已被证明是可判定的。后一个结果已在[8]中被利用，以证明相当表达的描述逻辑DL-4LQSR-1（D）的知识库存在可判定的一致性问题3语言3LQST0及其片段3LQSTR我们首先定义一个更通用的三级量化语言的语法和语义，表示为3LQST0。然后，在第3.1节中，我们表征3LQSTR-通过适当限制3LQST0-公式中量化器的使用来优化公式。三层量化语言3LQST0包括：(i) 单个（或排序0）变量的集合V 0，由x，y，z，.. . ;(ii) 集合（或排序1）变量的集合V 1，由X、Y、Z、.. . ;(iii) 集合（或排序2）变量的集合V 2，由A，B，C，.. . .除了变量之外，3LQST 0还允许形式{x1，. .......................................................，xk}（有限枚举），其中x1，.，x，k是两两不同的个体变量，k <1。3LQST0-quantier自由原子公式被分类为：• 级别0：x = y，x∈X，X ={x1，.，xk}，{x1，.，xk} ∈A，其中x，y，x1，.，xk∈V0，k1，X∈V1，A∈V2;• 水平1：X=Y，X∈A，其中X，Y∈V1，A∈V2。3LQST0纯泛公式被分类为：• 0级：（z1）（zn）0，其中0是0级量化器的命题组合自由原子和z1，. ........ ，zn∈V0，其中n1;3• 级别1：（Z1）. （Zm）1，其中1是任何水平的无量化器原子公式和0水平的纯泛公式的命题组合，Z1，.，Zm∈V1，其中m1.最后，3LQST0的公式都是无量化器的原子公式和0级和1级的纯泛公式的命题组合[3]在命题组合中允许使用的逻辑联结词是常用的：否定<$、连词<$、析取<$、蕴涵→和双蕴涵参与。72D. Cantone，M.Nicolosi-Asmundo/Electronic Notes in Theoretical Computer Science 322（2016）69为了便于阅读，我们将写（mzz1）. （zn）0和（z1）. （Zm）1是<$（z1）.的缩写。（zn）<$0和<$（Z1）. （1。3LQST0-解释是一对M=（D，M），其中D是对象的任何非空集合，称为M的域或论域，M是3LQST0的变量上的赋值，使得• Mx∈D，对每个变量x∈V0;• MX≠D，对每个集合变量X∈V1;• MApow（D），对于所有集合变量A∈ V2;4• M{x1，. ，xk}= Def {Mx1，. ，Mxk}。接下来，设M =（D，M）是3LQST 0-解释，并且设x1，.，xn∈ V0，X1，.，Xm∈V1，u1，.，un∈D，且U1，.，Um∈pow（D）.B y M[z1/u1， . . ，zn/un，Z1/U1， . . ，Zm/Um]定义了3LQST0-i迭代MJ=（D，MJ），使得MJzi=ui（对于i = 1，...，n），MJZj=Uj（对于j= 1，.，m），并且在其余变量上与M一致。另外对于对于任意VJ<$Vi（i= 0， 1， 2），设MVJ=Def{M <$：<$∈ VJ}.我我我在本文中，我们将使用缩写：Mz=M[z/u， .. . ， z/u]， MZ=M[Z/U， .. . ， Z/U]，定义1 1nn定义11m m其中变量zi和Zj、个体ui和子集Uj是从上下文理解的。设M是3LQST 0-公式，M=（D，M）是3LQST 0-解释。关于M（记为M）的可满足性的概念|=）在的结构上递归地定义。无数量算子的原子公式的求值是根据谓词“∈”和“=”以及有限枚举算子的标准含义进行的。一般公式解释如下：• M|=（z1）.. . （zn）0 iM[z1/u1， . . ，zn/un]|=0，对于所有u1，.，un∈D;• M|=（Z1）.. . （Zm）1 iM[Z1/U1， . . ，Zm/Um]|=101，对于所有U1，.，联合国教科文组织。最后，根据命题逻辑的标准规则对复合公式进行评价设f是3LQST0-公式。如果M| = 0（即， M满足），则称M是的3LQST0-模型。如果一个3LQST0-公式有一个3LQST0-模型，那么它被认为是满意的。如果所有3LQST0-解释都满足，则3LQST0-公式有效。4 我们记得pow（s）表示s的幂集。D. Cantone，M.Nicolosi-Asmundo/Electronic Notes in Theoretical Computer Science 322（2016）69730000000003.1限制性片段3LQSTR的表征3LQST R是所有3LQST 0-公式的集合，使得对于每一个纯单公式（Z1）. （Zm）1级的1发生在和每个纯通用公式（z1）. （zn）0级的0发生在1，条件n¬ϕ0 →Mzi∈Zj（1）i=1j =1是一个有效的3LQST 0-公式（在这种情况下，我们说，纯粹的普遍公式（z1）.（zn）0与变量Z1，.，Zm）。条件（1）保证，如果给定的解释赋值给z1，.，zn个使Z10为假的域元素，则所有这些值必须作为元素包含在分配给Z1，. 、Zm. 这一事实是出于技术原因引入的，它被用于引理5.7的证明（可以在[11]中的本文的扩展版本中找到），以确保满足性在有限模型中得到保留到目前为止，试图放松这种条件（仍然保持可判定性）的尝试下面的问题出现了：如何确定给定的3LQST0-公式是否是3LQSTR-公式？注意，条件（1）中既不涉及量化变量，也不涉及事实上，事实证明（1）是2LS公式，因此其有效性可以通过[15]中的决策程序进行测试，因为3LQST0是2LS的保守扩展。正如我们将在下一节中看到的，在大多数情况下，兴趣条件（1）只是基本命题重言式的一个实例<$（p→q）→p。在这种情况下，（1）的有效性仅仅通过检验就可以得出4语言的表达性3LQSTR初等集合论的几个结构在3LQSTR语言中很容易表达。特别地，可以用3LQSTR-公式表示受限 0 0变形的集前。这反过来又允许一个人表达另一个重要的集合，运算符，如二元并、交集、集差、集补、幂集运算符及其某些变体等。更具体地说，形式X={z：Z（z）}的集合形成器可以在3LQSTR中由下式（z∈XParticipants（z））（2）(in在这种情况下，它被称为3LQSTR）的0级可容许集合形成器，只要在将其变换为前束规范形式之后，所得到的公式满足3LQSTR的句法约束。特别是，当n（z）是3LQSTR的无量化器公式时，总是这种情况。在表1中，给出了3LQSTR的 0级可容许集形成子可表达的公式的一些例子，其中0和1分别代表空集和论域，·是关于论域的补算子。表1第一列中的公式74D. Cantone，M.Nicolosi-Asmundo/Electronic Notes in Theoretical Computer Science 322（2016）69000000000水平0的 3LQSTR的容许集形成子0X=0X=1X=YX=Y1Y2X=Y1Y2X=Y1\Y2X={z：z/=z}X={z：z=z}X={z：z∈/Y}X={z：z∈Y1<$z∈Y2}X={z ：表13LQSTR的0级容许集形成子可表示的一些文字。是在[15]中已被证明可判定的片段2LS（两级三段论）中允许的原子由于X={x1，.，xk}是3LQST R，2LS中的一个0级无量子化原子公式，有限枚举的2LS证明可以用3LQST R-公式表示.除了表1中的公式之外，以下文字ZX，|≤ h，|Z|h +1，|< h +1 ,| |h+1，|Z|= h（3）也可以用0级的3LQSTR-公式表示，其中h代表非负整数常数（参见表2）。事实上，所有的文字（3）都可以用0级纯泛3LQSTR-公式来表示，这些公式与变量Z有关，因此它们可以自由地用在形式为（Z）（Z）的1级泛公式的矩阵（Z例如，让我们考虑公式.（z1）. （zh+1）1≤i≤h+1zi∈Z→1≤i j≤h+1Σzi=zj（四）它表达了|Z|≤h。相对于变量Z，它的链接条件为：.¬1≤i≤h+1zi∈Z→1≤i j≤h+1Σzi=zj→1≤i≤h+1zi∈Z，这显然是一个有效的3LQSTR-公式，因为它是命题重言式<$（p→q）→p的一个实例，表明（4）与变量Z有关。 类似地，可以证明（3）中的其余公式也可以由与变量Z相关联的0级纯泛3LQSTR-公式表示。类似 的说 明也适 用于 形式A={Z ：Z （ Z ） }的集 合形 成器。 这 可以通 过3LQSTR-公式（Z）（Z∈AParticipant（Z））（5）（在这种情况下，它被称为3LQSTR的水平 1的可容许集合形成器），前提是（Z）不包含任何1类变量上的量化器，并且（Z）中所有0类量化变量都根据条件（1）与变量Z相关联D. Cantone，M.Nicolosi-Asmundo/Electronic Notes in Theoretical Computer Science 322（2016）697500000003LQSTR-公式0ZX，（n_z）（z∈Z→z∈X）、|≤ h（λ z 1）..|≤h(∀z1).. . （<$zh+1）zi∈Z→zi=zj|h +1|< h+1| |H+ 1| |0|= h|= h1≤i≤h+1|Z|≤h（|Z|D，d<$∈D <$$>，且VJ<$V1。 相对化解释当M的Rel（M，D，d，VJ）与D，d，和VJ之间的距离为M =1 1（D，M），使得.M=Mx， 如果Mx∈D<$d，否则MX=MXDM=.马波（D）\MΣJ{M<$X：X∈ VJ，MX∈M A}.为了便于标记，有时我们将省略对元素d∈D并简单地写Rel（M，D，VJ）来代替Rel（M，D，d，VJ）。Q1 1我们的目标是证明任何满足的3LQSTR-公式Rel（M，D，VJ）形式的小模型都满足，其中M=（D，M）是Rel，D是D的一个有界有限大小的子集，VJ<$V1是一个合适的集合有界大小的变量。例5.2考虑公式ψ≡(∀Z)(Z∈A↔(∃x1)(∃x2)(x1∈X1∧x2∈X2∧ {x1, x2}=Z))（z∈X1→z∈/X2）.V78D. Cantone，M.Nicolosi-Asmundo/Electronic Notes in Theoretical Computer Science 322（2016）691101101011111通过3LQST 0-解释M =（D，M）来满足，使得D ={0，1，. . }是自然数的集合，MX1={0，2，4，.. . }是偶数自然数的集合，M X2 ={1，3，5，.. . }是奇数自然数的集合，并且MA={{0，1}，{2，1}，{0，3}，{2，3}，. . . }是MX1的无序笛卡尔积，M X2。设Dj={ 0， 1， 2， 3， 4， 5}，d是Dj的任意元素，VJ={X1，X2}.然后，根据定义5。1，M_i=R_el（M，D_i，D_i，V_ J），其中R_i表示X_i，X_2，A如下：• MX1={ 0， 2， 4}，• MX2={ 1， 3， 5}，且• M={{ 0， 1}，{ 0， 3}，{ 0， 5}，{ 2， 1}，{ 2， 3}，{ 2， 5}，{ 4， 1}，{ 4， 3}，{ 4， 5}}。这是一个系统，以checkttM|我的天啊。我们首先陈述一个关于0和1级的无量化器原子3LQSTR给我5分。3LetM=（D，M）anddM=Rel（M，D，d，VJ）分别是M的一个3LQST0-解释和关于DD，d∈ D，且VJV1。此外，设K为固定正数，一个形式为x=y或x∈X的0级无量子化原子公式，其中x，y∈V0且X∈V1，一个0级无量子化的原子公式，X={x1，.，xk}或{x1，.，xk} ∈A，其中x1，.，xk∈ V0，X∈V1，A∈V2，k≤K，设k1是一个形式为X=Y的一X∈A，其中X，Y∈VJ，A∈V2。然后我们有：(a) 若Mx∈D0，则对任意x∈V0，在D0中，M|=100iM|=0;(b) 若（b1）Mx∈D<$，对任意x∈ V0，有（b2）M<$X = MX，若|MX|≤K，且|MX|>K，否则，对于每个X∈ VJ，并且（b3）M<$X= MX，对于X∈V1\Vj∈M，|=JiM|=BJ;10 0 0(c) 如果（c1）M≠X= MX，如果|MX|≤K，且|MX|>K否则，对于X∈ VJ，和（c2）（MXΔMY）ΔDΔnM|=101iM|=0.01。对于所有X，Y∈ VJ，使得MXi=MY，感兴趣的读者可以在[11]中找到前面引理的证明。根据命题逻辑，引理5.3立即蕴涵了下面的结果。第五章. 4LetM=（D，M）anddM=Rel（M，D，d，VJ）分别是M关于DD，d∈D，VJ<$V1的3LQST 0 -解释和相对化解释.此外，设K1和K2是以下类型的无量化器原子公式的命题组合：x = y，x∈X，X ={x1，.，xk}，{x1，.，xk} ∈A，X = Y，X∈ A使得[5]我们记得Δ表示由s Δ t =（s\t）<$（t\s）定义的对称差分算子。D. Cantone，M.Nicolosi-Asmundo/Electronic Notes in Theoretical Computer Science 322（2016）69791111101• Mx∈D<$，对于<$1中的每一个水平0变量x;• k≤K;• X∈VJ，对于出现在λ中的第一级无量子化原子公式（即形式X=Y或X∈• MX= MX，如果|MX|≤K，且|MX|>K，否则，对每个X∈ VJ;• （MXΔMY）D对所有的X，Y∈VJ，使得MXMY;nM|=ifndoifM|=0。前面的推论立即产生了以下类型的无量化器原子公式的命题组合的集合3LST0的一个小模型性质：x = y，x∈X，X ={x1，.，xk}，{x1，.，xk} ∈A，X = Y，X∈ A。事实上，设M是一个令人满意的3LST0-公式，M=（D，M）是它的一个模型同样，设K是任何有限枚举的最大长度{x1，.，xk}发生在设V和V分别是0级和1级变量的集合，0 1发生在1999年。我们构造了一个小模型，如下所示。设D1是D的基数不大于（K+1）的子集·|V|并且使得|JD1|m i n （K=1，|J|），对于每个J∈MV<$。对于每一对变量X，Y∈ V，使得MXi=MY，1 1选择元素dXY∈MXΔMY。 然后我们把D=M.d：X，Y∈V，MXMY}DDefV0{XY11并在D中选择任意元素d。那么，由推论5.4可以得出，相对论化的定义式M∈=R∈L（M，D∈，V∈）是一个 小模，因为|≤| V|+（K + 1）·|V|+的|V|二、|2. 事实上，通过适当地选择元素，01 1dXY在MX Δ MY中，我们可以强制约束|D|<|V|+（K+2）·|V|（ 请参阅0 1[5]）。综上所述，以下结果成立：引理5.5（3LST 0 -公式的小模型性质）设λ是3LST 0-公式，即，下列类型x = y，x∈X，X ={x1，.，xk}，{x1，.，xk} ∈A，X = Y，X∈ A。同样，设K是任何有限枚举的最大长度{x1，.，xk}发生以为单位，设VV是排序为0和排序为1的分别发生在两个月内当且仅当它满足于一个3LQST 0-解释M =（D，M），使得|D|<|V|+（K+2）·|V|.0 1由于有界域上的3LQST0-解释是有限的，并且它们可以有效地生成，所以3LST0-公式的可满足性问题的可判定性如下。80D. Cantone，M.Nicolosi-Asmundo/Electronic Notes in Theoretical Computer Science 322（2016）691011111101011111X... . ，Xm1X... . ，Xm1X，Xm1为了说明量化公式的主要结果，即对于纯泛3LQSTR-公式0或1，在关于D和VJV1的适当条件下，M=（D，M）的相对化的初始化公式M=Rel（M，D，d，VJ）也满足R（参见下面的Mz，λ=M，z=Def Rel（Mz，D，d，VJ）M[z/u， .. . ， z/u]定义1 1n nMZ，= Def Rel（MZ，DZ，dZ，VJ）M，Z=M[Z/U， .. . . ， Z/U]。Def11 mm引理5.6设M=（D，M）是3LQST0-解释，K是固定正的number，D<$$>D，d<$∈D<$，VJ其中，Vj=Rel（M，Dj，dj，VJ），M= MX，如果|MX|≤K，且|MX|>K，否则，对于每个X∈ VJ。此外，设（1）...... （n）n =0是一个纯通用的0级3LQST R-公式使得(i) Mx∈D0，对任意x∈V0在其中自由发生;(ii) 每个枚举项{x1，. ，xk}的大小至多为K（即， k ≤ K）;(iii) M<$X= MX，对于每个X中的变量X，使得X∈ V1\ VJ。nM|=（z1）.. . （zn）0=M|=（z1）.. . （zn）0.引理5.7设M=（D，M）是3LQST0-解释，DD，d∈D，VJ<$V1，M=Rel（M，D，d，VJ），K1，anddlet（Z1）. . （Zm）1是一个完整的1 1通用3LQSTR- 1级公式，（i）Z1， . . ，Zm∈/VJ;(ii) X∈ VJ，对于每个变量X∈ V1在（X ∈Z1）中自由发生. （λZm）λ1;(iii) Mx∈D<$，对于每一个变量x∈ V0在（Z1）中自由发生. （λZm）λ1;(iv) MX= MX，如果|MX|≤K，且|MX|>K，否则，对每个X∈ VJ;(v) （MXΔMY）<$D<$/=<$，对于所有X，Y∈ VJ使得MXi=MY ;(vi) 每个枚举项{x1，.，xk}的大小至多为K;(vii) 对于每一个 纯通用的 公式（1）. （zn）0级的0发生在1和变量X1，.，Xm∈VJ，使得M|=（（z1）. （zn）0）Z1，.，Zm，reareu1， .. . ，un∈D∈uchtM[z1/u1， . . ，zn/un]|=（0）Z1，. . ，Zm;6nM|=（Z1）.. . （Zm）1=M|=（Z1）.. . （Zm）引理5.6和5.7的证明可以在[11]中找到。6 给定一个公式和变量X1，. .，Xm，Z1，. ..，Zm，由Z1，...，Zm我们的意思是得到D. Cantone，M.Nicolosi-Asmundo/Electronic Notes in Theoretical Computer Science 322（2016）6981通过对每个i ∈ {1，. 、.、m}。82D. Cantone，M.Nicolosi-Asmundo/Electronic Notes in Theoretical Computer Science 322（2016）69000000000DNFDNFDNFDNF063LQSTR-公式的可满足性问题我们将解决3LQSTR的满意度问题，如下所示：(a) 首先，我们将把3LQSTR-公式的可满足性问题有效地减少到归一化3LQSTR-合取的相同问题（这些将被分解）。（以下简称为）。(b) 其次，我们将证明正规化的3LQSTR-合取集合享受着一个小型的样板房根据（a）和（b），3LQSTR的可满足性问题的可解性如下立即6.1归一化3LQSTR-合取设R是3LQSTR的一个公式，R 是R的一个析取范式. 我们观察到， DNF的析取是3LQSTR-文字的合取，即0级和1级的无量化器原子公式或它们的否定，以及0级和1级的纯泛公式或它们的否定，满足连接条件（1）。通过对变量进行适当的重命名，我们可以假设在CSDNF的同一个析取中，没有绑定变量可以出现在一个以上的quantier中，并且没有变量可以在同一个析取中同时出现绑定和自由在不破坏满足性的情况下，我们替换形式为（ （zn）0和<$（Z1）. （Zm）1分别通过它们的否定矩阵<$0和<$1出现在DNF中，因为对于任何给定的3LQST 0-解释M =（D，M）oneasM|=<$（z1）.. .（n =zn）如果M[z1/u1， . . ，zn/un]|=<$10，对于某个u1，.，un∈D，同样，M|=<$（Z1）. （m）n =1当且仅当M[Z1/U1， . . ，Zm/Um]|=1001，对于U1， . . ，Um∈pow（D）. 然后，我们将得到的公式恢复为析取范式，如上所述消除形式<$（z1）.的剩余负文字。（zn）0，这可能是通过前面消除形式为<$（Z1）.的负文字而引入的。（<$Zm）<$1，并再次将所得公式转换为析取范式。让我们是这样得到的公式请注意，上述所有步骤均保留满足性，所以我们的初始公式是满足的，当且仅当是满足的。此外，公式是满意的，当且仅当至少有一个分离这是一个很容易的事情来检查，每一个disunjunct的是一个连接3LQSTR-以下类型的文字（I，II，III）：x= y，x ∈ X，X ={x1，.，xk}，{x1，.，xk} ∈ A，<$（x = y），<$（x∈ X），<$（X ={x1，.，xk}），<$（{x1，.，xk} ∈A），X = Y，X ∈ A，<$（X = Y），<$（X∈A），（一）D. Cantone，M.Nicolosi-Asmundo/Electronic Notes in Theoretical Computer Science 322（2016）6983000001111其中x，y，x1，.，xk∈V0，X，Y∈V1，A∈V2;（z1）. （n）（II）其中n1和n0是无量子化的0级原子的命题组合;并且（Z1）. （μZm）μ1，（III）其中m1和m1是任意水平的无量子化原子公式和0水平的纯泛公式的命题组合，其中m1中的（mz1）型命题分量. （n =zn）n =0与约束变量Z1，.、Zm.我们称这样的公式为正规化的3LQSTR-合取。上述讨论可以总结为以下引理。引理6.1 3LQST R-公式的满足性问题可以有效地归结为3LQST R-合取的满足性问题。6.2归一化3LQSTR-合取的小模型性质设M是一个标准化的3LQSTR-合取，并假设M=（D，M）是一个M的模型。我们展示了如何从M中构造一个有限小的3LQST 0-initepreferatioM=（D， M），其中它是一个模的f。 我们准备了一份文件。公司简介我们概述了一个建立非空有限宇宙D的过程，仅取决于k，并且可以先验地计算。然后，根据定义5.1，我们将d3LQST0-inter r关系M=（D， M）转化为一个合适的变量集合VJ，并证明它满足λ。6.2.1宇宙的构造D设V、V和V是出现的排序为0、1和2的变量的集合，012设K是最小整数，使得k≤K，对每个有限枚举项{x1，.，xk}，发生在我们通过下面的过程构造域D假设1.1，...，h是形式（III）的的合取词。对于每个这样的合取项i（Zi1）.（Zimi）i，我们将集合i1，.，ni i的纯普遍原子公式的0级出现在其矩阵ni，并调用变量Zi1，.，Zimi的参数为1，.、阿吉尔岛然后我们把Φ i=Def{Φij：1 ≤i≤h且1 ≤j≤ li}。通过将[5]中描述的过程Distinguish应用于集合MV，可以构造一个集合D0，• MXD0对于所有的X，Y∈ V，使得MXi=MY，• |≤| V|-1。|− 1.84D. Cantone，M.Nicolosi-Asmundo/Electronic Notes in Theoretical Computer Science 322（2016）690Xi，.Xi101100000接下来，我们构造一个集合D1，使得|JD1|min（K=1，|J|），每J∈MV<$。很明显，我们可以假设|D1|≤（K+1）·|V|.1 1然后，在将D初始化为集合MV（D0<$D1）之后，我们插入D元素u1， .. . ，un∈D，u c hth atM[z1/u1， .. . . ，zn/un]|=（0）Z1，. . ，Zm1m，对于每个ε∈Φε，形式为（z1）. 具有Z1，..，Zm作为参数，并且对于每个有序m-元组（Xi，.，Xi）的变量，使得M|=Z1，.，Zm。1m1Xi1，. Xim上述结构容易产生，|≤| V|+（l + 2）·|V| − 1+ N·|V| L|Lψ ·|Φ ψ|、（7）01 1其中，L和N分别是Φ中任何纯泛公式的1级量化器的最大数量和Φ中纯0级泛公式出现在Φ1中的任何1级纯泛公式中。因此，一般来说，域D的大小与输入公式的大小成指数关系。6.2.2相对化的正确性LetM=Def Rel（M，D，d，V）. 下一个定理，其证明可以在[11]，statethatifM|=，thenM|=0。定理6.2设M是一个3LQST 0-解释，满足一个规范化的3LQST R-连接. 进一步地，letM=Rel（M，D，d，V）由根据定义5.1定义的3LQST0-interpretatin表示，其中D如上所述构造，V是C级缓存的v a ria b e nollec t i o n o le ct i o n o le c t i o le c t i on o le c t i o le c t i o n ole c t i o le c t i o le d i o le d i o le e d i o le d i o le e d i o le d i o le e d i o le d i ole陈文美|=0。上述还原和相对化步骤容易产生以下结果：推论6.3片段3LQSTR具有小的模型性质（因此其满意度问题是可以解决的）。与[10]类似，可以定义3LQSTR的一类子理论（3LQSTR）h，其中h2具有NP完全满足性问题。 除了某些语法约束（见[10]），（3LQSTR）h-公式中的所有quantifier前缀的长度都由常数h限制。事实证明，这样的子理论是非常有表现力的：事实上，在第4节中考虑的几个集合论结构（例如幂集算子的一些变体）可以用它们来表达。此外，可以示出模态逻辑S5可以在（3LQSTR）3中表示。7无序笛卡尔积给定集合X1，.，Xn，无序笛卡尔积X1≠. n是集合X1... Xn=定义、、、{x1，.，xn}：x1∈X1，.，xn∈Xn.D. Cantone，M.Nicolosi-Asmundo/Electronic Notes in Theoretical Computer Science 322（2016）69850i=10那么，A = X1.（8）其中A是2级变量，X1，...，Xn是水平1的变量，可以由3LQST R-公式表示..ΣΣ（简体中文）nZ∈A←→（x）... （2000年）x∈X{x，.，x}= Z.（九）1ni=1i i1n人们可能想知道是否有可能在不使用有限枚举运算符的情况下（因此，通过3LQSR-公式）表达笛卡尔乘积（8）由于原子{x1，.，xn}= Z可以由3LQS R-公式表示（z）（z∈Z参与z=xi），（1