多模态逻辑KM中的Craig插值及其构造性证明与上界的描述

可在www.sciencedirect.com在线获取理论计算机科学电子笔记354（2020）3-16www.elsevier.com/locate/entcs关于多模态逻辑Km的Everardo Bárcenasa，1 José-de-Jesús Lavalle-Martínezb，2Guillermo Molero-Castilloa，3Alejandro Velázquez-Menaa，4墨西哥国立自治大学墨西哥城b墨西哥普埃布拉贝内梅里特自治大学摘要式Craig插值定理是数学逻辑课程中一个众所周知的性质，具有许多领域的应用，例如在形式规范和本体论的模块化中。这个性质陈述如下：给出一个含义，说公式φ隐含另一个公式ψ，那么就有一个公式β，在φ和ψ的通用语言中被称为插值，因此φ也隐含β，就像β隐含ψ一样。 虽然已经知道多模态命题逻辑KmEnjoys Craig插值是一个很好的例子，我们没有意识到提供插值器的显式构造的方法。 我们在本文中描述多模态逻辑K m上Craig插值性质的构造性证明。可以从证明中显式地计算插值器。此外，我们还描述了用于计算插值的上界。该证明是基于前原技术在树超序列计算中的应用而进行的。作为插值的推论，我们还显示了Beth de finability和Robinson联合一致性。关键词：Craig插值，多模态逻辑KM，树超序列，Beth可分解性，Robinson联合一致性。1介绍性Craig插值、Beth definability和Robinson联合一致性是逻辑语言语法和语义学关系中众所周知在本文中，我们在命题多模态逻辑KM的背景下研究了所有这些逻辑概念。Craig [4]为经典第一阶逻辑提供了第一个插值考虑一个公式φ意味着另一个公式ψ，插值性质1电子邮件地址：ebarcenas@unam.mx2电子邮件地址：jlavalle@cs.buap.mx3电子邮件地址：gmoleroca@fi-b.unam.mx4电子邮件地址：mena@fi-b.unam.mxhttps://doi.org/10.1016/j.entcs.2020.10.0021571-0661/© 2020作者。出版商：Elsevier B.V.这是CC BY许可证（http://creativecommons.org/licenses/by/4.0/）下的开放获取文章。4E. Bárcenas et al./理论计算机科学电子笔记354（2020）3存在一个公式β，称为插值，在φ和β的通用语言中，它被假定为非空的，因此φ意味着β，而β意味着ψ。{\displaystyle {\}插值在计算机科学中的应用最近已经被研究用于形式验证[22]、计算复杂性[3]和知识表示[15，28]等。虽然我们已经知道命题多模态逻辑KmEnjoys Craig插值，但我们并不知道提供插值的显式构造的方法，这在许多计算机科学应用中是至关重要的[22，15，28]。在本文中，我们给出了多模态逻辑Km的Craig插值定理的构造性证明。该证明意味着一种用于计算插值的直前向算法此外，我们还讨论了这种计算的复杂性。由一对公式φ（p1）和φ（p2）组成的隐式定义意味着p1和p2是逻辑等价的，其中p1和p2分别是出现在φ中的命题变量。一个显式定义在于公式φ（p）隐含p在逻辑上等价于由φ中的元音组成的另一个公式ψ（不考虑p）。在大多数常见的逻辑语言中，它是直接向前的，即显式的定义和隐含的定义。然而，皈依者并不总是坚持下去。这种相互关联的含义被称为Beth definability属性。Beth在[1]中的经典第一阶逻辑中首先观察到了这个性质。Craig插值和Beth definability有时是等价的，这取决于逻辑语言。在本文中，我们描述了如何在插值函数的帮助下从隐式定义构造显式定义。一致性也是逻辑语言中的一个常见概念给出两个一致的逻辑理论（公理系统、知识库等）;就一个常见的词汇而言，人们很自然地会想知道这些理论是否也是一致的。如果在一种逻辑语言中，这个理论的联合是一致的，我们就说这个语言具有罗宾逊联合一致性的性质。我们还表明，这个性质是在Km的上下文中插值的结果。1.1相关工作在[5]中，本文报道了模态逻辑中插值性质的早期研究。[8，18]。在[8]中，Gabbay为包括K和S在内的几个单模态逻辑提供了插值。Maksimova在[18]中确定了拓扑布尔代数和包含S4的模态逻辑中的可合并性的紧密联系，并规定只有有限数量的包含S4的模态逻辑才能享受插值。Maksimova后来在[19]中通过合并提供了所有范式逻辑的插值这个结果在[16]中被扩展到多模态逻辑。在[21]中，马克思用一种基于双模拟的技术为几种模态逻辑提供了插值。这项工作包括K的插值证明，纤维模态逻辑，以及知识和信念的多模态在上述所有作品中，插值都是由语义学或代数方法提供的。虽然这些方法是非常通用的，并且可以应用于数逻辑，但是它们不提供插值器的显式构造在E. Bárcenas et al./理论计算机科学电子笔记354（2020）35在当前的论文中，我们为多模态逻辑提供了插值的综合证明KM. 该证明包括插值器的显式构造。模态逻辑KB、KDB、K5和KD5的合成插值证明在[24]中描述。在这项工作中，插值是通过一个无切割的完整序列表状演绎系统的手段提供的。模态逻辑K和T的构造性插值在[2]中给出。更准确地说，在这项工作中提供了一种更强的插值形式，称为均匀插值。在统一插值中，插值词由隐含公式的通用语言组成，但受到命题变量的一个选择的限制。最接近我们论文的作品是[7]。在这项工作中，构造性插值提供了整个模态立方体，由K，D，T，B，5和4的任意组合的逻辑结果组成。本工作中使用的证明技术是基于嵌套序列的。在我们的论文中，我们得到了一个构造性插值证明的多模态逻辑KM，使用Maehara技术在一个无割完备树超序列演算。在[9]中，广泛报道了模态逻辑中可分解性、插值性和一致性的关系。特别地，描述了单模态逻辑和直觉逻辑的几个可判定性结果这些结果是通过代数方法获得的，根据[9]的作者的说法，代数方法也可以应用于多模态逻辑[10]。我们在本文中表明，作为插值的直接结果，Km也具有Beth de finability属性。这个证明也是构造性的，因为我们可以在KM中计算插值，所以我们也可以从隐式定义中构造显式定义。在目前的工作中，我们还间接地证明了一致性与插值的帮助下，通过构造一个矛盾组成的插值的不一致联盟的两个理论。另一个相对较新的关于模态类逻辑中可定性的研究可以在[28]中找到。在本文中，Beth definability是在描述逻辑的背景下在计算机科学中的应用，如查询重写，也被讨论。可定义性是通过一种允许计算显式定义的表格方法的手段来提供的。此外，还描述了该方法的计算成本。[10]我们还描述了一个上界的插值计算在KM。1.2大纲首先，我们在第2节中介绍了多模态逻辑KM。在第3节中，我们描述了Km的完全无割树超序列计算。然后，在第4节中，通过Maehara技术的手段，我们从Km含义的树超序列证明中提取插值在本节中还提供了关于插值器构造的2 EXPTIME上限。在第5节中，作为插值的结果，我们还证明了Beth de finability和Robinson联合一致性。最后，在第6节中，我们给出了文章的摘要，并简要讨论了进一步的研究观点。2多模态逻辑在本节中，我们介绍了多模态逻辑KM的语法和语义，然后我们提出了一个相应的希尔伯特式证明系统。6E. Bárcenas et al./理论计算机科学电子笔记354（2020）3M。| ∀∈∈m我们假设一个基本的模态语言：一个非空的命题集PROP;和一个非空的有限模态集MOD。定义2.1[语法]公式的集合由以下语法归纳地定义：{\displaystyle {\}φ= p |φ|φ ε φ |Qmφ其中p是一个命题，m是一个模态。符号：T：=p ι κp：= υ Tφ υψ：=ά（φ φ τ υψ）φ→ψ：= φφ υψ Qmφ： =QmφKripke结构是一个三元组M=（W，R，V），其中：• W是一个称为定义域的非空集;• R是二进制关系Rm的有限集合：W×W，对于每个模态m;以及• V：PROP›→2W是将命题映射到域子集的赋值函数。定义2.2[语义学]给定一个克里普克结构=（W，R，V），公式解释如下：[[p]]M={w她家V（p）}[[φ]]M=W\[[φ]]MM=[[φ]]M[[φ ]]M[[ψ]]M[[Qφ]]M=wwJW：if（w，wJ）RM，然后wJ她家[[φ]]MWem a，也写M， w|=φinsteadofw她家[[φ]]M|=φ当M中的e v是w时，我们有M，w|=φ，在这种情况下，我们说M是φ的模型。如果任何Kripke结构是φ的模型，我们写|= φ。定义2.3[希尔伯特导出系统]我们通过以下方案和规则来定义导出系统H，对于每个m≥MOD：A1φ→（ψ→φ）A2（φ→（ψ→β））→（（φ→ψ）→（φ→β））A3（φ→φ）→（φ→φ）A4Qm（φ→ψ）→（Qmφ→Qmψ）R 1 φ→ψ φψR2φQmφ我们说公式φn可从H导出，写为►Hφn，如果有一个序列φ1，φ2，...，φn，因此对于每个i她家她家{1，...， n}：E. Bárcenas et al./理论计算机科学电子笔记354（2020）37►►• φi是H中schema的另一个实例，向上替换，或• 这里有（are）j当一个序列S出现在一个树T中时，更准确地说：• S[ST]，其中TJ或ST。我们按预期扩展树之间的发生关系T：• T=TJ;E. Bárcenas et al./理论计算机科学电子笔记354（2020）39¬∧¬∧MM• （S[ST]），当ST时;• （m：TJ，STJ）;以及• （m：TJJ，STJ），提供TJJTJ和STJ：• （S[ST]）;以及• （mJ：TJJ，STJ），前提是m/= mJ或TJJ/惊呼TJ，STJ。我们说序列S发生，在模态m下，在树超序列m1：T1，m2：T2的有限序列中，...mk：Tk，当有一个i这样，mi是m，Ti有形式S [ST]。此外，我们经常写S[m：SJ]而不是S[ST]，提供SJ发生在ST中的m之下。定义3.5[树-超序列导出系统]树-超序列G的导出系统定义如下：{\displaystyle {G}。• 初始树超序列数：• 命题规则（PropositionalRules）：TS，φLTφ，STφ，ψ，SLTφψ，S• 模态规则：TT<φ，S>RTS，φTTRTTQLTQRT在G中，规则顶部的树超序列被称为前提（premises）。树-规则底部的超序列被称为"结论"（conclusions）。一个没有前提的规则的实例被称为树超序列公理（tree-hypersequent-axioms）。我们现在将派生树的概念定义为根据G的规则构造的树，因此节点是由树超序列组成的。[10]派生树的根上的树超序列被称为端树超序列（end-tree-hypersequent）。派生树的叶子上的树超序列被称为初始树超序列（initial tree-hypersequents）。G中树超序列T的证明是一个派生树，其中所有的初始树超序列都是树超序列公理，并且终止树超序列是T。如果在G中有T的证明，我们也说T在G中是可导的，我们写►GT。现在考虑实例化A4的以下证明：10E. Bárcenas et al./理论计算机科学电子笔记354（2020）3-L-R∧¬∧¬T<φ，ψ►ψ>T<φ►ψ，φ>T<φ►ψ，►ψ> RT<φ ►ψ，φτ άψ>Qm−（φτ εψ），Qmφ►[m：ά（φτ εψ），φ►ψ]QLQm−（φτ άψ），Qmφ►[m：φ►ψ]Q−（φτ άψ），Qφ►[m：►ψ]MQmLM MQMRQm−（φτ άψ），Qmφ►QmψLQm²（φ τ εψ），Qmφ，Qmψ ►LQm²（φτ εψ）QmφτQmψR►► （Qm²（φτ εψ）QmφQmψ）在证明中，第一个时间规则QmL应用于Qmφ，而第二个时间规则应用于Qm（？（φ？？ψ））。我们现在回忆说，树超序导数系统相对于希尔伯特导数系统是健全和完整的。定理3.6（[25，23]）对于任何序列S，►GS，if且仅if，►HS。因此，从定理2.4和3.6直接向前看，树超序导数系统是正确的。推论3.7对于任何序列S，►GS，if且仅if，|=SI。我们通过回顾树超序漂移系统的复杂性来结束这一节。定理3.8（[23]）对于任何给定的序列S，判定►GS在2EXPTIME中。4插值法我们在本节中给出了我们的主要结果，Craig插值Km。我们遵循前原最初提出的一种建设性技术[17]。 由于Km可以被看作是用Qm运算符扩展的经典命题逻辑，所以从综合的观点来看，我们的证明在所有布尔情况下都与前原对经典偏序逻辑的证明相匹配。 然而，在此之前，此技术无法推广到Qm运算符的规则。这是因为，直到引入我们论文中描述的无割树超序列系统之前，还不知道满足子公式性质的类似序列的推理系统[23]。我们首先定义了公式φ的一组非逻辑符号Sym（φ），如下所示：• Sym（p）={p};• Sym（φ）=Sym（φ）;• Sym（φψ）=Sym（φ）Sym（ψ）;• Sym（Qmφ）={m}{\displaystyle {m}}{{\displaystyle {\displaystyle{\}一个（多个）公式集的一组非逻辑符号的定义与预期的一致。E. Bárcenas et al./理论计算机科学电子笔记354（2020）311∧<<<<<<为了技术上的方便，我们考虑导数系统G的等价外延GJ，其中公式T被考虑为本身（而不是作为符号）。G中的所有规则在GJ 中 也是一样的。此外，首字母序列T也包含在GJ中。引理4.1（前原引理）设T χ Δ可在G中导出，设χ 1、χ 2和Δ 1、Δ 2分别是χ和Δ的部分。然后有一个公式β，称为插值，所以T <χ1► Δ1，β>和T<β，χ2►Δ2>可以在GJ 中导 出，并且Sym（β）（Sym（ 1）Sym（Δ1））（Sym（2）Sym（Δ2））。证明。 通过在证明树的高度上的归纳。基本情况是TP，Gamma Δ，p。 然后根据命题p在划分中的出现次数来定义插值β {\displaystyle\interpolant\beta}。在两个p分别出现这是明确的TT<− T，χ2 ►Δ2>对于下面的情况，我们只列出相应的划分和插值。T<χ1►Δ1，T>TTTT<χ1►Δ1，p， ά p>T<χp，p，χ2 ►Δ2>感应步骤...假设最后一个推论如下所示：T<χ ►Δ，φ>T<χ ► Δ，ψ>T<χ ► Δ，φψ通过归纳假设，存在用于上树超序列的插值因子β1和β2根据φ和ψ在各自分区中的出现次数，有两种可能的情况，每种情况下，在推理规则的顶部都有一棵树超序列。然后，我们有以下四个证明：T<χ1►Δ1，φ，β1>T<β1，χ2 ►Δ2>T<χ1►Δ1，ψ，β2>T<β2，χ2 ►Δ2>T<χ1►Δ1，β1>T<β1，χ2 ►Δ2，φ>T<χ1►Δ1，β2>T<β2，χ2 ►Δ2，ψ>根据φ ψ在分区中的出现次数，我们构造了插值函数。φas以下内容：T<χ1►Δ1，φκψ，β1υβ2>T<β1υβ2，χ2 ►Δ2>T<χ1►Δ1，β1β2>T<β1β2，χ2 ►Δ2，φψ现在考虑最后一个推论如下：T<χ，φ，ψ►ΔTT<β，χ2 ►Δ2>T<χ1，φ►Δ1，β>T<β，ψ，χ2 ►Δ2>T<χ1，ψ►Δ1，β>T<β，φ，χ2 ►Δ2，T<χ1►Δ1，β>T<β，φ，ψ，χ2►Δ2>因此，无论分裂发生在哪里，φψ，β也是插值的：T<χ1，φ−ψ►Δ1，β>T<β，χ2 ►Δ2>T<χ1►Δ1，β>T<φτψ，β，χ2 ►Δ2>如果最后的推论涉及对权利的T然后我们有了以下通过归纳法进行插值的方法T<χ1，φ►Δ1，β>T<β，χ2 ►Δ2>T<χ1►Δ1，β>T<β，φ，χ2►Δ2>It is then clearβ也是否定的插值T<χ1►Δ1，β， φ>T<β，χ2►Δ2>T<χ1►Δ1，β>T<β，χ2►Δ2， εφ>我们以类似的方式进行另一个归纳步骤，包括左边的否定：TT我们通过归纳法得到了以下插补β：T<χ1►Δ1，β[m： ►φ，ST]>T <β，χ2►Δ2[m： ►φ，ST]有两种情况取决于Qmφ在分区中的出现次数：T<χ1►Δ1，Qmφ，−Qmφτβ[ST]>T<χQmφτβ，χ2 ►Δ2[ST]>T<χ1►Δ1，Qmφ χβ[ST]>T Q定理4.2（Craig插值）对于任意两个公式φ和ψ，if|=φ→ψ，那么就有一个公式β，这样|=φ→β，|=β→ψand Sym（β）Sym（φ）Sym（ψ），前提是存在一个命题p，使得p恰好恰好是Sym（φ）Sym（β）证明。假设|=φ→ψ，然后根据推论3.7，φ►ψ在G中可导。根据引理4.1，有一个公式β，其中φ►β和β►ψ在Gj中是可推导的。设p≥Sym（φ）≥Sym（ψ）。现在，让βJ通过替换T由β得到（p）（p）。直接向前看，φ ►β和β►φ可在G中导出，并且hence（根据推论3.7）|=φ→β和|=β → ψ。Q从定理3.8和引理4.1，它也是立即获得一个上界的插值计算。推论4.3（复杂性）计算Km插值是在2EXPTIME。5可定义性和一致性Beth de finability属性存在于这样一个事实，即隐式de finability意味着显式definability。我们首先证明了这个性质也持有Km作为克雷格插值的直接推论。[10]此外，作为插值的直接结果，我们证明了KmEnjoys Robinson联合一致性，其中指出两个一致公理系统（理论）的并集，就它们的公共字母表而言，是一致的。定义5.1 [隐式可定性]设φ（p，p1，...，pk）是一个公式，其中p，p1，...，pk是在其中出现的命题。我们说φ（p，p1，...，p（k）的p隐式if其中PPJ.|= (φ(p, p1,..., pk）φ（pJ，p1，...，pk））→（ppJ）定义5.2 [显式可确性]设φ（p，p1，...，pk）是一个公式，其中p，p1，...，pk是在其中出现的命题。我们说φ（p，p1，...，p（k）明确地定义p，当|=φ（p，p1，...，pk）→（pψ）其中Sym（ψ）Sym（φ（p，p1，...，p（k））\{p}14E. Bárcenas et al./理论计算机科学电子笔记354（2020）3►定理5.3（Beth De finability）设φ（p，p1，...，pk）是一个公式，其中p，p1，...， pk是在 其中出现的命题。如果φ（p，p1，...，p（k）从p隐式结束，然后φ（p，p1，...，p（k）明确定义p。证明。 从隐含的可定义性假设来看，很容易看出这一点。|=（φ（p，p1，...，p（k）（p）（p）（p）（p）（k）（p）（p）（p）p（k）→p（J）根据Craig插值定理4.2，我们得到了|=（φ（p，p1，...，p（k）→ p（p）→ψ|=ψ →（φ（pJ，p1，...，p（k）→p（J）其中Sym（ψ）Sym（φ（p，p1，...，p（k））\{p}Q在定义一致性的概念之前，我们需要对一些概念进行精确的描述公理系统是一组有限的公式。公理序列是公理系统的一个（pos-siblyempty）子集我们说一个序列S在G中可从一个公理系统A导出（可证明），如果有一个公理序列AJofA，那么►GAJ，S.定义5.4[一致性]一个公理系统是不一致的，如果空序列可以从它推导出来。我们说一个公理系统是一致的，如果它不是不一致的。定理5.5（罗宾逊联合一致性）考虑两个一致公理系统-项A1和A2，如果对于任何公式φ，使得Sym（φ）Sym（A1）Sym（A2），如果不是φ和φ都可以分别从A1和A2（或A2和A1）导出的情况，则A1A2是一致的。证明。 我们证明了相反的观点。 如果A1A2不一致，则分别存在A1和A2的两个公理序列Aj1和AJ2。因此，A1，A2可导出为G. 记住A1和A2都是一致的，那么就不是空的。根据引理4.1，有一个插值φ，其中Sym（φ）Sym（A1）Sym（A2），因此A1►φ和φ，A2►（henceA2►φ）都可以在Gj中导出。在定理4.2的证明中，直接向前证明了A1►φ和A2►φ也可以在G中通过将T在φ中的所有出现替换为−（p−p）得到a p她家（A1）−Sym（A2）而导出。Q6结论虽然我们已经知道多模态逻辑Km具有Craig插值性质[21]，但在本文中，我们给出了Craig插值性质的构造性证明。该证明是基于前原技术的一个完整的无割树超序列计算器。一个插值算法可以很容易地从证明中推断出来。据我们所知，以前并不知道Kminterpolants的这种明确构造。插值器的构造在许多情况下都是重要的，例如作为知识表示和形式验证，作为一种模态化过程[28，22]。受这些应用程序的启发，我们还描述了一个E. Bárcenas et al./理论计算机科学电子笔记354（2020）3152EXPTIME上行链路用于插值计算。一个较低的限制肯定是一个有趣的进一步研究方向。插值器的计算也可以应用于从隐式定义中构造显式定义中。[10]我们还描述了一个类似的构造，以证明Km的Beth可分解性定理。 众所周知，显式定义的计算在查询重写算法中是重要的，其应用领域广泛到计算机科学中的几个领域[28]。因此，我们明确了将插值大小复杂性作为未来工作的动机。在 模 态 逻 辑 K 的许 多 时 间 扩 展 中 ， 插 值 是 不 常 见 的 。在 线 性 时 间 逻 辑（LTL）、计算树逻辑（CTL）和CTL中，插值失败[20]。这也是具有共同知识的认识论逻辑的情况[27]。命题动力学逻辑（PDL）的插值一直是一个非常难以捉摸的问题。Leivant [14]首次提出了PDL的时间插值法。然而，Kratch注意到了这个证明中的一些问题[13]。后来，Kowalski [11]提出了另一个关于PDL的插值主张，他很快撤回了[12]。然而，PDL的插值无疑是一个非常有趣和具有挑战性的研究视角。μ-微积分的插值是已知的[6]。然而，它并不知道它的建设性证明。由于我们还不知道μ演算的无割类序列推导系统，因此将前原的技术推广到这个逻辑是不平凡的μ-演算插值的构造性证明也可能是一个有趣的研究方向。参考文献[1] 贝丝，E。W.，论帕多阿在[2] Bilková，M.模态逻辑中的一致插值和命题Quantificers，Studia Logica85（2007年）。[3] 库克，S. A.和R. A. Reckhow，命题证明系统的相对有效性，J.Symb. 日志。44（1979）。[4] 克雷格，W.，Herbrand-Gentzen定理在相关模型理论和证明理论中的三种用法，J.Symb。日志。22（1957）。[5] D'Agostino，G. 《非经典逻辑中的插值》，Synthese164（2008）。[6] D'Agostino，G.和M。霍伦伯格，《关于μ演算的逻辑问题：插值、林登和洛斯塔斯基》，《符号逻辑杂志》65（2000）。[7] 适合，M.和R. Kuznets，《通过嵌套序列进行，《纯粹应用逻辑年鉴》166（2015）。[8] Gabbay，D. M.，Craig霍奇斯，编辑，会议在数理逻辑-伦敦'70 。 讲座笔记在数学（1972年）。[9] Gabbay，D. M.和L. L. Maksimova，[10] Halpern，J.Y.和Y。摩西，知识和信仰的模态逻辑的完整性和复杂性指南，Artif。智能。54（1992）.[11] Kowalski，T.PDL具有插值，符号逻辑杂志67（2002）。[12] Kowalski，T. "PDL具有插值"的撤回注释16E. Bárcenas et al./理论计算机科学电子笔记354（2020）3[13] Kracht，M.[14] Leivant，D. 《命题动力学逻辑的理论方法论证明》，载于：J.Díazand I. Ramos，编辑，编程概念的形式化，国际学术讨论会，计算机科学讲座笔记107（1981）。[15] 卢茨，C.和F。Wolter，表达描述逻辑中均匀插值和遗忘的基础，in：T.沃尔什，编辑，IJCAI，第22届人工智能国际联合会议论文集（2011年）。[16] Madarász，J. 十、多模态逻辑中的Craig插值定理，《逻辑学部分公报》3（1995年）。[17] 前原，S.，《论克雷格的插值定理》，《朱雀12》（1960）。[18] Maksimova， L.， 《 模 态 逻 辑 中 的 插 值 定 理 和 拓 扑 布 尔 代 数 的 可 合 并 变 体 》 ， 《 代 数 与 逻 辑 》18（1979）。[19] Maksimova，L.，范式逻辑中的，Studia Logica50（1991）。[20] Maksimova，L.，具有"下一个"运算符的时间逻辑没有插值或beth属性，西伯利亚数学杂志32（1991）。[21] 马克思，M.，模态逻辑中的插值，in：A. M. Haeberer，编辑，代数方法学和软件技术，第七届国际会议，AMAST，学报，计算机科学讲座笔记1548（1998）。[22] 麦克米兰，K.L.，插值和模型检查，in：E.M. 克拉克，T.A. Henzinger，H.Veith和R. Bloem，编辑，模型检查手册。施普林格，2018年。[23] Munoz-Toriz，J. - P.，E.巴尔塞纳斯，我。马丁内斯-鲁伊斯和J. - R.- E. Arrazola-Ramírez，拉丁美洲和加勒比（S4）描述逻辑的（超）序列，计算和系统20（2016）。[24] 阮，L. A.、模态逻辑的分析表系统和插值KB，KDB，K5，KD5，Studia Logica69（2001）.[25] Poggiolesi，F. "模态逻辑的序列计算"，Ph.D.论文，佛罗伦萨大学，巴黎第一先贤祠-索邦大学（2008年）。[26] 罗宾逊，A.，《一致性的结果及其在定义理论中的应用》，《符号逻辑杂志》，第25期（1960）。[27] Studer，T. 常识没有最好的属性，Inf. Process.莱特。109（2009）。[28] Ten Cate，B.E. 弗兰科尼和我。Seylan，Beth de finability in expressive好战逻辑，J. Artif。智能。第48（2013）号决议。