S4模态逻辑中规则可容许性的检验方法

理论计算机科学电子笔记262（2010）17-32www.elsevier.com/locate/entcs一种检验S4中规则可容许性谢尔盖·巴别尼舍夫a，弗拉基米尔·雷巴科夫a，雷娜特·A.施密特b和德米特里·季什科夫斯基ba计算机和数学系，英国曼彻斯特城市大学b英国曼彻斯特大学计算机科学学院摘要可接受的规则可以用在逻辑的任何公理系统的任何推导中。 本文本文介绍了模态逻辑S4中规则的可容许性检验方法。 我们的方法是基于一个标准的语义基础的画面方法。特别地，我们将S4中的规则可接受性简化为扩展S4的逻辑中的公式的可满足性。扩展逻辑的特点是一类模型，满足一个变种的共同覆盖属性。这类模型可以通过定义良好的一阶规范来形式化。使用最近推出的合成tableau决策程序的框架，这可以变成一个健全的，完整的和终止tableau演算的扩展逻辑，并给出了一个基于tableau的方法来确定规则的可接受性关键词：表演算，容许规则，模态逻辑，S4，表综合框架。1介绍逻辑容许规则首先由Lorenzen [12]考虑。最初的研究仅限于观察存在不可导出的可接受规则的有趣例子（参见Harrop [7]，Mints [13]）。当Friedman [2]提出是否存在算法来重新认知直觉命题逻辑IPC中的规则是否是可接受的问题时，该领域获得了新的动力。这个问题和模态逻辑S4的相应问题在Rybakov [15，17]中得到了解决。同样的方法可以用于广泛的命题模态逻辑，例如K4，S4，GL[18]。Roziere [14]提出了一个解决方案，弗里德曼S4中的容许规则理论在严格意义上不具有有限逼近性质[11]。 [15]中的算法是基于存在一个模型（有界大小），见证了一个规则的不可接受性，但不是1571-0661 © 2010 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2010.04.00318S. Babenyshev等人/理论计算机科学电子笔记262（2010）17它必然是所有其他可接受规则的模型。在[1]中，观察到可以通过过滤获得见证模型规则的可接受性与统一问题有着直接的联系。一种改进的技术[18]用于元变量规则的可容许性、统一化、参数统一化以及逻辑方程的可解性 在传递模态逻辑中。一些传递模态逻辑和IPC的可容许性判定算法，基于投影公式和统一化，在Ghilardi [3，4，5，6]中有描述。 他们结合决议和tableau方法finding projectiveapproxima- tions的公式，并依赖于存在的算法定理证明。在[24]中描述了基于[5]中IPC算法构建的S4这些算法是专门为寻找匹配和统一问题的一般解决方案而设计的。 相比之下，[15]的原始算法可以在S4中只能找到这些问题的一些解决方案。在本文中，我们专注于S4，并介绍了一种新的方法来识别规则的容许性。我们的方法是基于减少的问题，在S4中的规则的可接受性，以满足一定的公式在S4的扩展。我们将扩展逻辑称为S4u，+。 S4u，+可以由一类模型来表征，这些模型满足可由模态公式定义的共同覆盖性质的变体。这个性质在一阶逻辑中是可表达的，并且意味着逻辑的语义可以在一阶逻辑中形式化。我们利用这一性质，以便在最近引入的框架中设计S4u+的 用于自动合成tableau演算和决策过程[21，22]。[22]的tableau合成方法工作如下。(i) 用户用一种多排序的一阶语言定义给定逻辑的形式语义，以使某些良好定义的条件成立。(ii) 该方法自动将逻辑的语义规范化为Skolemised蕴涵形式，然后将其重写为tableau推理规则。它们与一些默认的闭包和相等规则相结合以这种方式获得的规则集提供了一个健全的和建设性的完整演算。此外，这组规则自动具有关于有限子公式运算符的子公式属性。 如果逻辑可以证明 对于一个定义良好的一阶语义进行有限过滤，然后添加一个通用的阻塞机制会产生一个终止tableau演算[21]。我们展示了如何，使用这种方法，一个声音，完整的和终止表演算可以合成的扩展逻辑S4u，+。 这个表演算是然后将其并入S4中的规则容许性问题的求解方法中。本文的结构如下。在第二节中，我们定义了模态逻辑S4的句法和语义，以及它的带有泛模态的扩展S4u以这种方式，它们可以容纳在tableau综合框架中（22）。本节还定义了标准模态逻辑结构和概念所需的主要结果的文件。在第三节中，我们给出了S_4的可导规则和可容许规则的定义，并说明了检验可容许性的RybakovS. Babenyshev等人/理论计算机科学电子笔记262（2010）1719S4S4--连接词的定义背景理论你好ν（<$p，x）参与式ν（p，x）你好ν（p<$q，x）参与ν（p，x）<$ν（q，x）<$你好ν（Qp，x）参与式y（R（x，y）<$ν（p，y））<$x，y，z。R（x，y）<$R（y，z）→R（x，z）<$R（x，x）图1.S4中S4的语义的具体化在S4的规则。 将S4中的规则可容许性约化为S4u+中的可满足性在第4节中描述。在第5节中，我们展示了如何用一组一阶公式来表示co-cover性质的公式化变体，这些公式为在tableau综合框架中指定S4u，+在这个框架内，我们可以合成声音并完成逻辑S4u，+和S4u的表演算。 在一定条件下 可以对缺省生成的微积分规则进行细化[22]。这些条件对于我们所考虑的逻辑都是成立的，我们将在第6节中讨论。第7节描述了如何通过添加[20，21]的无限制阻塞机制来获得终止tableau演算。在第8节中，我们最后给出了一个检验规则可容许性的算法，以及在S4中检验规则可导性的算法。 在第9节中，我们将讨论该算法和方法对其他逻辑的适用性以及与可容许性密切相关的各种问题由于篇幅有限，我们省略了Tableau综合框架的一些细节;对此感兴趣的读者可以参考[22]和[20，21]。2语法和语义我们用LS4表示模态逻辑S4的语言。 L S4由标准模态语言在命题变量的可数集合{p，q，p0，q0，... . }，布尔逻辑连接词<$和<$，以及模态连接词Q。其他布尔连接词，如T、→和参与式，以及模态连接词Q，定义如下：和往常一样，q，Q设Lu表示具有“某处”模态的语言LS4的扩展⟨u ⟩. 对偶模态是通用模态，用[u]表示对于公式φ，我们用sub（φ）表示φ的所有子公式的集合。让sub（子）=def{sub（φ）} | φ∈ 对于任何一组公式，我们通常写--sub（φ1，...，（1），而不是（ φ1，...，φ n）。 一组公式被称为sig-natureisub（）=。根据[ 22 ]中的tableau综合框架，我们容纳L u中多排序一阶规范语言 这种规范语言包括一个可数集x，y，z，x0，y0，z0，. . 表示模型中元素的一阶变量的二进制谓词符号R，表示可及性关系的背景理论的二进制谓词符号R，以及表示强制关系的二进制（intersort）谓词符号ν| =. v可以被认为是一个holds谓词。图120S. Babenyshev等人/理论计算机科学电子笔记262（2010）17≈S4⊆\⟨⟩|∈|∈∈∈||∈∈|给出了框架中S4标准语义的一阶语义规范。我们用SS4表示规格。除了图1的公式，SS4还包括等式谓词的通常的同余公理，详见[22]。因此，（签名的）S4-（Kripke）模型是一阶模型M=在任意替换变量p和q的LS4-公式（来自签名）的情况下，验证图1的所有公式。设S4u是S4的某处（或普遍）模态的扩张S4u的语义规范，记作SS4u，是S4的规范SS4的扩展，(1)x（ν（这就定义了某处情态动词“u”。（签名的）S4 u模型通过定义是一阶模型M= WM，R M，ν M，其在任意替换L u公式的情况下除了验证图1的所有公式之外还验证了该公式。(from签名（签名）对于命题变量p和q。注意，如果M是签名M的模型，则M也是任何签名M的模型。在另一个方向上，很明显，通过（重新）定义ν对公式的解释（通过归纳它们的长度），每个较小签名的模型M都我们在定义模型时经常使用这些事实S4（resp. S4u）是一个一阶结构F=W F，R F，它验证了SS4（resp. SS4u）。模型M基于框架F（或M的基础框架是F）i = W M=W F且R M=R F。一个模型M的簇是一个集合U ∈ W M，使得对于所有的w ∈ W M和u ∈ U证明了（w，u），（u，w）∈RM i<$w ∈U. M的任何RM-不可比簇的集合称为M中的反链。一个簇U<$WM是极大的i <$（u，w）∈RM意味着对所有w∈WM和u∈U，w ∈U.设M是一个固定的签名，M是签名M的模型。我们说，一个公式φ在一个世界中是真的（满足的），WM（符号M，w=φ）i （φ，w）ν M。一个公式φ（来自φ）在M（用符号M=φ表示）i <$M，w=φ中对每一个w W M成立。并且，像往常一样，φ在M i中是可满足的，其中有w W M使得M，w=φ。公式φ在框架F（以符号F=φ表示）i中有效，它在基于F的签名的每个模型M中为真。对于一个签名ω和WM中的每个元素w，我们定义了w的一个π-型τ∈（w作为一套所有公式从numb是真的在w，即：τ（w） =def {∈| M，w| {\fn黑体\fs19\bord1\shad1\1cHD8AFAF\4cHC08000\b0}.如果从上下文中已知τ，则我们省略上标τ，而写τ（w）。一个签名M的模型M称为n-离散的i ∈ τM（w）= τM（v），其中对任意的w，v ∈ W M，w = v. 一个模型M是公式化的，对于每一个元素w ∈ W M，有一个公式φ，使得M，w| = φ和M，v| = φ对所有v ∈ W M\ {w}.很明显S. Babenyshev等人/理论计算机科学电子笔记262（2010）1721||||公司简介{ {\fnMicrosoft YaHei}如果模型是有限的，那么每个离散的模型也是公式化的。我们称签名的Kripke模型M为签名的Kripke模型N的可定义变体，如果M和N基于同一框架，并且对于每个命题变量p ∈ Kripke J，存在公式φ ∈ Kripke使得M，w| = p N，w| = φ对于每个w ∈ W M=W N。设n是n个变量p1，...，p n.一个S_4-模型M称为S_4 i-模型M的n -特征化模型|= φ φ ∈ S4，对于每个φ ∈ φ。3S4允许的规则由于S4的语言包含合取，在不失一般性的情况下，我们只考虑单前提规则。规则是一对α，β的S4-公式，通常写为α/β。规则r=α/β在模型M（记为M=r）i中是有效的，其中M=α蕴涵M=β。 一个规则r在框架F（记为F=r）上有效，ir在任何基于F的模型M中有效。 两个规则r1，r2在语义上等价，或简单等价，如果F| =r1F |= r2对于任何帧F。一个规则r=α/β在S_4中是可导的，i ∈β可由α导出，肯定前件规则和必然性规则。 很明显，R是在S4中可导的，则在每个S4-模型中都成立。S4中的演绎定理的以下变体可以通过标准方法证明定理3.1规则α/β在S4 i中可导出，且[u] α ∈ β在S4u中不满足。规则r=α/β对于模态逻辑S4是可容许的，记为r∈Adm（S4），如果对于从σ（α）∈S4的每个替换σ，有σ（β）∈S4。一系列公式化和n-特征化的S4模型Chn（S4），n>0在[18]中描述。这些模型用于描述以下容许标准。定理3.2（定理3.3.3的推论[18]）一个规则在S4中是可容许的，如果它在Ch n（S4）的一个可定义变体中有效，对于每个n> 0。本文结果最重要的性质是模型Chn（S4），n>0及其可定义变体具有共覆盖性质。S4的容许规则可以由具有共同覆盖性质的模型类来刻画，如[16]所示。一个更一般的结果出现在[18，定理3.5.1]中。IPC的类似表征结果出现在[9，定理4.1（iv）]和[10，推论3.14]中。通过定义，模型M具有共覆盖性质（CCP），如果对于每个有限反链DW M（D可以为空），则存在一个单元素簇WWM使得{u ∈ W M|（w，u）∈ R M}={w}<$ {u ∈ W M|（v，u）∈ R M}.v∈D22S. Babenyshev等人/理论计算机科学电子笔记262（2010）17.p∩∧↔∈∩{|∈}单元素簇称为D的共覆盖。注意，空反链的共覆盖是M的最大单元素簇。一个规则r被称为是在约化正规形式，如果它具有以下形式（rnf）r=1≤j≤sφj/p0，且eaCh析取φj具有以下形式φj=0≤i≤nt（i，j，0）i0≤i≤n（Qpi）t（i，j，1），其中（i）所有φj都是离散的，（ii）p0， . ，pn表示比例变量，（iii）t是布尔函数t：{0，.，n}× {1，.，s}× {0，1} → {0，1}（即，t（i，j，z）∈ {0，1}），以及（iv）α0d=ef<$α andα1=defα fora nyfor mulaα.使用重命名技术，任何模态规则都可以转换为简化范式中的等价规则[15]。引理3.3任何规则r = α/β都可以在指数时间内转化为约化范式的等价规则。证明我们描述了[ 18 ]的算法（引理3.1.3和定理3.1.11）。 设r=α/β是一个规则。我们需要一组新的变量q γ γsub（α，β）。 第一步是将r=α/β替换为r1=α（q β β）/q β。 很容易看出，r在框架F上是可反驳的，r1可以在同一个框架F上被反驳。因此r和r1是等价的。归纳步骤：假设规则ri=γ i/q β在第i步得到。我们称一个公式δsub（γi）sub（α，β）final，如果它不是变量，也不是sub（γi）sub（α，β）中任何其他公式的真子公式。设Ti是第i步得到的所有最终公式的集合。我们用一个新的规则代替规则ri，即ri+1=γ i+1/q β，其中γi+1=ti（γi）qγ<$qδ∈Ti（（qγParticipy）<$（qδParticipδ））<$<$qδ，Qqδ∈Ti（qδParticipateδ），ti（γi）是由γi通过用δ替换所有最终子公式而得到的公式qδ。 可以直接检查ri和ri+1是否等价。注意，每个归纳步骤都减少了规则的非布尔子公式的最大高度。因此，经过有限个步骤，我们得到一个前提γk，它是形式为p或Qp的文字的布尔组合，其中p是一个命题变量。我们用do（r）表示这个中间形式（深度为1的形式）。最后，将所得到的规则rN=γk/qβ的前提转化为文字上的析取范式.这只需要变量数量的指数时间，即，关于原规则的子公式的数目，这与任何布尔公式到析取范式的约简相同QS. Babenyshev等人/理论计算机科学电子笔记262（2010）1723iQj我⇐⇒CIMM1221我 J我J在引理3.3中得到的约化正规形是唯一定义的，记为rnf（r）。注意，引理3.3证明了比r和rnf（r）的等价性更多的东西。特别地，从证明中可以得出，如果r在模型N中是可反驳的，则rnf（r）在N的可定义变体M中是可反驳的，其中M，w| = q γ N，w|对于所有的γ ∈ sub（α，β），设r是一个约化正规形式的ny规则。 令Θ（r）d=ef{φ， . ， φ}be，1sr的所有析取的集合F或eveφj∈Θ（r），令θ（φj）d=ef {p|t（i，j，0）=1}和θ（φ）d=ef {p|t（i，j，1）=1}。也就是说，θ（φj）表示r的变量的集合，其中p为φj中的共现，并且θQ（φj）是r的变量pi的集合，其中Qpi在φj中出现。历史上，识别S4的可接受规则的第一个算法是基于下一个定理。它的公式需要下面的定义，它取自[15]。对于析取算子W ∈ Θ（rnf（r））的每个子集，设M（rnf（r），W）表示其中W M=defW的Kripk模型，RMd=ef{（φ，φ）|θ（φ）θ（φ）}和（p，φ）∈νMdefp∈ θ（φ）。定理3.4（定理3.9.6 [18]）规则rnf（r）对于S4是可容许的，如果对于任何集合W Θ（rnf（r）），模型（rnf（r），W）不具有以下性质中的至少一个。（a1）Re是φj∈W使得M（rnf（r）， W），φj|=p0.（a2）M（rnf（r）， W），φj|=φj，其中llφj∈W。（a3）F或M的任何子集D，则存在φj∈W，使得θQ（φj）=θ（φj）<$θQ（φ）。φ∈D注意，在（a3）中，D可以是空的。定理3.4意味着我们可以使用该算法来识别S4[15]中规则r步骤1. 将规则r简化为深度一形式do（r）。步骤2. 从do（r）构造简化形式rnf（r）。步骤3.对于rnf（r）的析取集的每个子集W，检查定理3.4的条件是否成立。步骤4.如果定理3.4的条件（a1）对于S4是不容许的，否则r对于S4是容许的。步骤1可以在多项式时间内完成，步骤2可以在指数时间内完成，步骤3可以在指数时间内完成。 这意味着，该算法由长度为r的双指数函数限定。 基于[8，9]中的技术的更详细的复杂性分析意味着S4的规则容许性问题是coNExpTime-完全的[10]。QQ24S. Babenyshev等人/理论计算机科学电子笔记262（2010）17.S4S4Σ∧¬ ∧¬def4可受理性的语义表征现在我们给出S4中容许性的语义特征。我们说一个S4u-模型满足公式可定义的共同覆盖性质，如果以下（无限）公理集成立（对于n>0）：（FCCP）<$x<$p（ν（Qp，x）→ν（p，x））x1···ν（Qp，x）→（ν（p，x）<$ν（Qp，x1）<$· ·<$ν（Qp，xn））.设SFCCP是由（FCCP）公式和SS4u中的公式组成的语义规范。设FCCP（k）是签名k的所有S4u-模型的类，这些模型满足SFCCP公式在Lu-的替换下的所有实例命题变量的计算公式设S_4u+为模态逻辑，语言L_u以S_FCCP为语义规格。下面的定理是上述定义的直接结果，以及所有n-特征模型Chn（S4）满足（FCCP）公式的事实。定理4.1 S4u，+是S4的保守扩张。现在我们证明S4u，+具有有效有限模型性质。设M是一个固定的签名，M是签名M的S4u +-模型我们定义过滤（通过）模型M如下。在集合WM上的等价性定义为：def defwτ（w）= τ（v）。此外，[w]={v ∈ W M|w v}和W M={[w] |w ∈W M}。接下来，RM=def{（[w]，[v]）|M，v|=表示M，w|=Q对于每个Q∈}并且，最终y，νM=def{（k，[w]）|（ω，w）∈νM}，对于每一个ω∈ω.下面的引理可以通过验证SFCCP中的所有语义条件都成立，通过对S FCCP中公式的结构进行归纳来证明引理4.2（过滤引理）M是签名M的S4u +-模型。注意，根据定义，M是离散的，并且只要M是有限的，它就是有限的。定理4.3（等效有限模型性质）设φ为公式，n为φ的长度（即， φ中的符号数）。 如果φ在（签名子（φ）的）S4u，+-模型中是可满足的，那么它在（签名子（φ）的）有限S4u，+-模型中是可满足的，并且它的大小不超过2 n。定理4.4α/β ∈ Adm（S4）iβ在S4 u，+中是不满足的。证明假设α/β是不可容许的，且p1，...，pn是出现在α和β中的所有命题变量。然后存在模型M-Chn（S4）的可定义变体，使得M| = α/β。该模型具有共覆盖性质，并且常规地将M变换为满足[u]αβ的S4u +-模型。或相反，设f=defsub（[u]αβ），且假设[u]αβ满足于S4u，+-型号。然后，它在一个有限的非线性离散的S4u，+-模型M中是满意的（S. Babenyshev等人/理论计算机科学电子笔记262（2010）1725defqγ⇐⇒⇐⇒S4S4∃∧没关系∧→ΣS4∀1··· ∀我很 抱 歉 。1 ···def（签名），过滤引理。 设subQ（α，β）={Qγ|γ ∈ sub（α，β）}sub（α，β）对任意的LS 4-公式α和β.对任意w∈WM，令τQ（w）=def{γ∈亚Q（α，β）|M，w| = γ}且φ（w）=γ∈sub（α，β）χ（γ）γγ∈sub（α，β）Qqx（Qγ），其中x是集合τQ（w）的特征函数让我们考虑一下模型Md=efW M 其中WM=def {φ（w）|w ∈ W M}，（φ（u），φ（v））∈RMdef（u，v）∈RM，且（qγ，φ（w））∈νM<$defM，w| = γ。每个φ（w）都是一个约化正规形式RNF（R）中的析取所以我们有，• WM θ（rnf（r）），•M的基本框架同构于M的基本框架，• M满足定理3.4的条件（a1）根据定理3.4，rnf（r）是不可容许的，因此r也是不可容许的。Q5合成Tableau演算现在我们应用[22]的方法来生成S4u，+的一个合理的和构造性的完备表演算。为了应用该方法，我们必须确保S4u，+的语义规范SFCCP在[22]的意义下得到良好的定义。首先，SFCCP必须在以下意义上规范化：（i）所有指定语义的公式都是Lu-开的，即，它们不包含命题变量的量化器，(ii)SCCP中的所有公式被分为三组：逻辑联结词语义的肯定和否定定义，以及施加框架条件的背景理论。还要求背景理论中的所有公式不包含任何非原子模态项。SFCCP中Lu连接词的每个定义（图1和（1））都可以是分为两个含义。由此产生的公式集可以分为所需的两组正连接定义和负连接定义。第三组，背景理论的S4u，+，由公式指定的反射性和传递性的关系R和（FCCP）公式。规范SFCCP归一化的主要困难是非原子模态项Qp的出现和变量p在（FCCP）中的量化为了解决这个问题，我们首先将每个公式ν（Qp，y）替换为其语义等价物z（R（y，z）ν（p，z）），并将所得公式转换为前束范式。这给了我们：x p y（R（x，y）v（p，y））v（p，x）x x x p y z R（x，x）R（x，x）（R（x，y）v（p，y））→.ν（p，x）.这些公式仍然不是[22]中所要求的Lu-开公式，因为26S. Babenyshev等人/理论计算机科学电子笔记262（2010）17分解画面规则：1x1···R（g n（x1，.，xn），x1）<$· ·<$R（g n（x1，.，x n），x n）理论场景规则：ν（<$p，x）<$v（p，x）ν（p<$q，x）ν（p，x）|ν（q，x）ν（Qp，x）R（x，fQ（p，x）），ν（p，fQ（p，x））ν（u p，x）ν（p，fu（p））x<$xR（x，x）<$v（<$p，x）ν（p，x）<$v（p<$q，x）<$v（p，x），<$v（q，x）v（<$Qp，x）<$R（x，y）|<$v（p，y）v（<$u<$p，x），y<$y<$v（p，y）xx，yy，zz<$R（x，y）|<$R（y，z）|R（x，z）无限（FCCP）表规则集（n >0）：（cc0）：pp，y<$R（g0，y）|<$v（p，y）|v（p，g0）（ccn）：x1x1，.，xn<$xn，y <$y0R（gn（x），x1），.，R（gn（x），xn）（ccn）：pp，x1x1，.，xn<$xn，y<$y<$R（gn（x），y）|<$v（p，y）|v（p，gn（x））|R（x1，hn（p，x，y）），ν（p，hn（p，x，y））|···关闭画面规则：ν1（p，x），<$ν1（p，x）⊥R（x，y），<$R（x，y）⊥图2. 为S4u，+在P上的量化器。然而，使用Skolemisation可以消除公式中p-quantifier之前的所有现有quantifier，然后我们可以省略p的quantifier。此外，我们将长公式分为两部分。我们得到：(FCCPJ）不稳定。（R（g0，y）<$ν（p，y））→ν（p，g0）<$.Σ1.·· ·（R（gn（x1， . ，xn），y）ν（p，y））→v（p，g n（x1，...， x n））<$（v（p，z）<$（R（x1，z）<$···<$R（x n，z）.这里，gn（n≥0）表示引入的Skolem符号。我们使用符号SJ表示从SFCCP其中，对于mulaFeChCP的所有（FCCP）均由对于以下各项的相应（FCCPJ）替换：mulae。显然，对于每个一阶结构M，SFCCP 和SJ的泛闭包在M中是等价的。 所以S. Babenyshev等人/理论计算机科学电子笔记262（2010）1727变换后的语义SJ等于FaCleCnPt到SFCCP，并公理化了这一点类模型。FCCP现在我们准备从SJ合成tableau演算。 所生成tableau规则如图2所示。符号fQ，fu，FC、CP表示Skolem函数，g0表示Skolem常数。gn hn设T是由图2中的规则和图3中列出的相等的标准tableau规则组成的tableau演算。等式表规则从等式同余公理中获得，这些公理总是包含在任何语义规范的背景理论中，参见[22]。28S. Babenyshev等人/理论计算机科学电子笔记262（2010）17分解画面规则：∃∃S4R（x，y）xx，yy<$R（x，y）xx，yy<$v（p，x）pp， xxν（p，x）pp， xxR（x，y），x<$zR（z，y）R（x，y），y=zR（x，z）ν（p，x），x<$yν（p，y）xyxxy，yzxz图3.出现在SS4u中的谓词的相等全等规则。给定一个公式φ，并假设我们的目标是确定φ的可满足性，任何表推导的开始是公式ν（φ，a），其中a是一个任意常数a，它不会出现在T的规则中。a可以被看作是公式x ν（φ，x）中引入的x的Skolem常数。微积分的规则以熟悉的方式自上而下地我们从[21，22]中假设以下定义。设T表示表演算，φ是公式.我们用T（φ）表示一个用于检验φ的可满足性的完备表导子。也就是说，表推导中的所有分支都被完全展开，并且T的所有适用规则都应用于T（φ）。 像往常一样，我们假设，微积分的所有规则都是非确定性的。如果应用了闭合规则，则Tableau派生的分支是闭合的，否则该分支称为开放的。 表导子T（φ）是闭的，如果它的所有分支都是闭的，并且T（φ） 否则是开放的。 一个演算T是可靠的（对于逻辑L），对于任何公式φ，每个T（φ）是开的，只要φ在L-模型中是可满足的。T是完备的，如果对于任何不满足的公式φ，存在一个闭的T（φ）。T是构造完备的（对于L），如果对于T中的一个完备表导子中的任何开分支，可以从分支的项构造一个L-模型，使得该模型反映分支中出现的所有公式。（构造性完备性是比完备性更强的概念。称T是终止的，如果T中的每个已完成的开表导子都有一个有限的开分支。很容易检查S4u，+的指定SJ在的意义[22]。 [22，T定理F1CaCn Pd2]的一个推论就是这个结果.定理5.1 T是S ~ 4 u ~+的一个可靠的构造完备的微积分。6一种改进的Tableau演算生成的演算T可以被重新定义如下。 首先，可以通过将某些规则中的否定结论移动到前提位置来改进演算。我们将只包含命题变量而不包含任何复模态项的公式向上移动。对于每一条规则，不难检查[22，定理3]中给出的保持可靠性和构造完备性的条件是否为真。第二，我们可以应用[22，第5节]中描述的第二种细化。 为此我们把语言L u 通过引入可数集合{i，j，k，.. . 名义上的}变量和逻辑连接词（作用于名词），对应于Skolem函数和常数。可以引入和指定@算子，使得对于每个名义项i和对于扩展的S. Babenyshev等人/理论计算机科学电子笔记262（2010）1729∨⟨ ⟩¬¬∨¬¬⟨ ⟩⊥≈≈≈（续）：1@Qk≥1（）：@i（pq）@ip|@iq@iQp（Q）：@iQfQ（p，i），@fQ（p，i）p（u）：@iup@fu（p）p（）：@ip@ip（）：@i<$（pq）@i<$p，@i<$q（Q）：@i<$Qp，@iQj@jp（u）：@i<$up，@jj@jp理论场景规则：@我我(re（C）：@iQi（transs）：@iQj，@jQk@iQk（FCCPJ）表规则的无限集合（n>0）：(ccJ0）：（ccJ0）：@g0Qi，@ip0@ g0 g01@g0p（ccJn）：@i1i1，. . ，@inin@gn（i）Qi1，. 在gn（i）Qin（ccJn）：@gn（i）Qj，@jp@gn（i）p|@i1Qhn（p，i，j），@hn（p，i，j）p|·· ·|@inQhn（p，i，j），@hn（p，i，j）p关闭画面规则：（）：@ip，@i<$p⊥图4. 针对S4u+的（回复）：@ip@我我（sym）：@ij@ji（transs）：@ij，@jk@ik@ip，@ij0@jp（con）：@iQj，@jk我图5.精化的等式同余规则语言）。不难看出，扩展语言的所有连接词的语义都可以用语言本身来表示（见[22，第5节]）。综上所述，我们得到的细化规则如图4所示。 在这些规则中，i，j，k，i1，.，i n表示名义变量，fQ，fu，g n和h n（n 0）表示与Skolem 函数同名的“名义函数”。设T+是表演算，它由图4的规则和图5中给出的精化等式规则组成。在T+中，030S. Babenyshev等人/理论计算机科学电子笔记262（2010）17分解画面规则：检验φ的可满足性的一个表式推导从公式@i0φ开始，其中i0是一个新的标称常数。定理6.1 T ~+是S_4u ~+的一个可靠的构造完备表演算。S. Babenyshev等人/理论计算机科学电子笔记262（2010）1731⟨ ⟩⟨⟩∧¬∧ ¬ ∧ ¬我∧¬我007终止Tableau演算我们在定理4.3中证明S4u+具有有效有限模型性质时使用了一个过滤参数。也就是说，在[21]的术语中，S4u+允许有限过滤。使用[21]的结果，这意味着在第5节和第6节中生成的表演算可以变成终止表演算。特别地，我们只对精化演算T +感兴趣。将以下无限制阻塞规则添加到T+中，得到一个终止表演算。@ii，@jj（ub）：@ j |@<$j阻塞必须满足的条件是：（b1）规则（Q）和（u）从不分别适用于形式为@ iQj和@ iu j的公式，其中j是名义项。（b2）如果@ij出现在分支中并且i j（即，在推导过程中，名词i严格早于名词j出现），然后所有进一步应用产生新名词的Tableau规则（在我们的例子中，（Q），（C u n），（cc J0）和（cc Jn））规则）到出现j的公式的操作不在分支内执行。(b3)在每一个开放的分支中，都有一些节点，产生新名词的任何Tableau规则的任何应用（即，（Q），（ub）规则的所有可能的应用都具有00被执行。我们用TS4u，+表示扩展的微积分。由于T+对于S4u，+和S4u，+是合理的和构造完备的，所以[20]中的结果允许我们声明：定理7.1 TS4u，+是S4 u，+的可靠的、（构造性）完备的和终止的表演算。设TS4u是由与TS4u相同的规则集组成的表演算但不包括（FCCPJ）规则：（ccJ0）、（ccJ0）、（ccJn）和（ccJn）。应用工作表0101以类似的方式合成到S4u得到以下结果。定理7.2 TS4u是S4 u的可靠的、（构造性）完备的和终止的表演算.8一种检验规则可容许性的Tableau方法把所有的结果放在一起（特别是定理3.1，4.4，7.1和7.2）是用于确定模态规则在S4中是否可接受的方法。步骤1.给定一个S4-规则α/β，将其改写为[u]α β。步骤2.使用表演算TS4u来检验[u]α β在S4u中的可满足性。步骤3. 如果TS4u（[u]α β）是闭的，即，[u]α β在S4u中是不可满足的，然后停止并返回30S. Babenyshev等人/理论计算机科学电子笔记262（2010）17≈≈1¬¬∧¬¬⟨ ⟩ ¬ ∨ ¬ ¬0∧ ¬⊥2（0（0=01. @i<$u（<$Qp <$$>Q<$p）.......................给定31.@iQi4（Q），18：def4Q<$p，i2）2. @i0i0（received），1...............................3. @i0<$（<$Qp<$$>Q<$p）（<$u），1，24. @i0<$$>Qp（<$s），3..............................5. @i0<$$>Q<$p（<$p），3.......................6. @i0Qp（<$），4..............................................7. @i0Q<$p（<$），5.........................................32.@i4<$p......................................................（Q），1833.@i4i4.. . . （re）），3234.）@i0i3（ub），2，30.................35.@i3i0（sym），34.......................36.@i2Qi0（con1），28，35.37.@i2Qi2（transs），11，36.8. @iQi1（Q），6：...................def1季度038.）@i2i4...............................................（ub），13，330i=f（p，i）..................9. @i1p（Q），6....................................................10. @i1i1.. . . . . （re）），911. @iQi2..........................................（Q），7：i2deffQ（<$p，i0）12. @i<$p（Q），7................................................满意在S4u......规则不是可衍生的 ......39.@g0g0...................................................................（ccJ0）40.@g0 <$（<$Qp <$$> Q <$p）（<$u），1，35213. @i2i2（receiving），12.......................41.@g0 <$$> Qp.............................. （<$s），4042.@g0 <$$> Q <$p.........................（<$p），4014. @i2<$（<$Qp<$$>Q<$p）（<$u），1，13............................................................................15. @i2<$$>Qp（<$），14...........................43.@g0 Qp..............................................（<$），4144.@g0 Q <$p..................................... （<$），4216. @i2<$$>Q<$p（<$p），14...................17. @i2Qp（<$），15..........................................45.@g0 Qi5 .......（Q），43：defi5=fQ（p，g0）18. @i2Q<$p（<$），16....................................46.@i5p.....................................................（Q），4319. ）@i0i1.....................