拓扑混合逻辑的定理证明实验

理论计算机科学电子笔记231（2009）309-321www.elsevier.com/locate/entcs拓扑混合逻辑的定理证明实验Dmitry Sustretov，Guillaume Ho Muslimann，CarlosAreces，and Patrick Blackburn塔拉里斯INRIA洛林54602Villers-l`es-Nancy，Francefirstname. loria.fr摘要本文讨论了拓扑解释下混合逻辑定理证明的两个实验。我们首先讨论混合逻辑的拓扑解释，并注意到它增加了什么，正统模态逻辑的拓扑解释。然后，我们研究两个实现的证明方法。第一个使用HY LO BAN，这是一个终止定理证明器，用于搜索获胜的搜索策略在某些以拓扑为动机的博弈中第二种是基于预防的方法，该方法利用HY-L O T AB[16]，标准关系解释下的混合逻辑的基于表格的定理证明器。我们比较了这两种方法，并指出了一些进一步工作的方向保留字：混合逻辑，拓扑语义，定理证明1介绍模态逻辑的拓扑语义比关系语义（现在的标准）早20年;此外，它是第一个证明模态逻辑的深层技术结果的框架。Alfred Tarksi所有拓扑空间然后，在1944年，McKinsey和Tarski [11]证明了一个优雅的结果：S4也是通常拓扑下实数的模态逻辑在20世纪60年代关系语义学诞生后，拓扑语义学在某种程度上被忽视了，尽管技术上有趣的结果继续被证明（例如参见Esakia [6]和Shehtman [13]）。然而，最近，部分由于对空间逻辑和发展知识拓扑学的兴趣日益增长，人们的兴趣又恢复了;Aiello，van Bentham和Bezhanishvili [1]是这种工作的一个很好的例子。 在这个新阶段强调的一个主题（特别是由van Bentham和他的各种合著者）是需要超越基本的就像他们指出的1571-0661/© 2009由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2009.02.043310D. Sustretov等人/理论计算机科学电子笔记231（2009）309然而，基本语言对于数学家感兴趣的拓扑空间的种类是高度缺乏表达力的。事实上，这一点从上面提到的麦肯锡和塔斯基的经典结果中已经很清楚了。实数（在通常的拓扑下）满足拓扑学家所称的T0和T1分离公理，以及其他许多公理;也就是说，实数是一个具有许多特殊拓扑性质的空间。然而，基本模态语言认为这个空间和所有拓扑空间的类之间没有区别;两者共享相同的模态逻辑，即S4。最近的工作表明，当基本模态语言被混合逻辑的基本工具（即名词）丰富时，事情变得更加有趣 和普遍模式。正如我们将在下面讨论的，增加的表达性意味着所有拓扑空间、T0拓扑空间和T1拓扑空间的所有拓扑空间都是不同的。但是这种增加的表达能力对定理证明有影响。关于普通模态逻辑的拓扑定理证明没有什么需要说的-它但是混合逻辑的定理证明还没有得到很好的发展。特别是，目前没有终止证明器处理逻辑丰富的最小混合逻辑K，或应付的普遍形式。现在，我们的目标是将拓扑定理证明与IN TO HY LO（推理工具，混合逻辑;见[2]）混合逻辑的一般推理框架这样做将需要有效的终止工具来处理S4模态、名词、通用模态和拓扑动机约束。在这里，我们报告的两个初步实验，我们认为指出这样的实施方式。这两种方法都是基于Sustretov但这两种方法不同地利用了Sustretov• 首先，我们讨论了一个基于游戏的证明者称为H Y L O B AN，直接实现Sustretov的基于游戏的证明的PSPACE的完整性的逻辑的T 0和T1空间。 这种方法的好处是保证了终止并且基于游戏的基础架构似乎是独立的兴趣;其缺点是（目前）它是极其不成熟的。• 第二种方法利用了一个事实（Balder ten Cate指出），即Sustretov约简中使用的有限帧的相关类别可以在通用模态的帮助下进行编码。因此，我们可以将拓扑满足性问题转化为涉及泛模态的关系满足性问题，并使用HY LO TAB[16]解决它们，H y L o T ab是唯一能够将S4模态与泛模态和名词一起处理的现有证明器。这种方法被证明比目前的HY- LO BAN的实现更有效;它的缺点是HY LO TAB不是一个优化的证明器，并且不能保证在所有输入上终止我们按以下步骤进行。第二节讨论了混合逻辑的拓扑语义，以及T0和T1空间的混合公理化。 在第3节中，我们介绍 基于博弈的拓扑定理证明方法及其实现D. Sustretov等人/理论计算机科学电子笔记231（2009）309311≡ ¬ ¬ ≡ ¬ ¬∧P在HYLOBAN。 在第4节中，我们讨论了基于预防的方法和基于HY LO TAB的方法。在第5节中，我们评估了这两种方法，并在第6节中得出结论。2混合逻辑我们假设读者熟悉关系解释下的混合逻辑的基础知识（例如，[4]包含了所有需要的背景知识）。在这里，我们将使用基本的混合语言，但在另一种语义下：公式将在拓扑空间上解释我们将使用的语言是由以下语法生成的φ：：= p|我|φ ∧ φ |¬φ |Qφ|Eφ其中p是一个普通的命题字母，i是一个被称为名词的特殊命题字母。我们用字母p qr... 对于普通命题变量和i，j，k，. . . 对于nominals我们像往常一样定义对偶模态Q和A：QφQφ和Aφ E φ，有时我们将E（i φ）写成@iφ 名词和Eφ构成了正统模态语言的基本混合扩展。要求Nominal总是评估为单例集，并且Eφ被解释为因为 这种解释的混合机是相当普遍的，并已最经常使用的经典关系解释的模态算子。正如我们现在将要看到的，这些思想直接转移到情态的拓扑学处理上定义2.1（拓扑模型）拓扑空间是一对（T，τ），其中 τ（T）使得T τ和τ在有限交和任意并下是闭的。τ的元素称为开集或开集，包含点x的开集称为点x的邻域。开 集的补集称为闭集。一个拓扑模型M是一个元组（T，τ，V），其中（T，τ）是一个拓扑空间，赋值V将命题字母和名词映射到T的子集，其中名词总是被分配为单例子集。定义2.2（拓扑语义学）公式φ在拓扑模型M（记为M，w）中的点w处的真值|=φ）归纳定义如下：M，w |= pi x∈V（p）M，w |= ii x∈V（i）M，w| = φ=φ我的M，w| = φ和M，w|=M，w |=<$φiM，w$φM，w |= Qφi <$ $ >O∈τ使得w∈O且<$v∈O。（M，v| = φ）M，w |= Ei M，v|=312D. Sustretov等人/理论计算机科学电子笔记231（2009）309|∃||→因此，对于所有的名词i，M，w=@ i i vM，v=i和M，v=，就像在关系语义中一样。在这种解释下，我们对混合逻辑有什么了解？首先，所有拓扑空间的混合逻辑与关系语义下传递自反框架的混合逻辑一致：即两者都是混合S4。然而，它 事实证明，混合机器对两个最简单的分离公理是敏感的，这两个公理是定义拓扑学家称之为T0和T1空间的条件定义2.3（分离公理）对于任意两个不同的点x，y，存在x的开邻域不包含y，或者y的开邻域不包含x;任何单例集都是闭的.这两个条件在混合语言中都是可以定义的式@i<$j→（@iQ<$j<$@jQ<$i）定义T0空间类，并且Qi→i定义了T1空间类。我们将这些空间的混合逻辑记为Log（T0）和Log（T1）. 很容易看出，每个T1空间都是T0空间（但反之则不然）因此Log（T0）是Log（T1）的真子集让 这在其关系解释下可能是熟悉的：我定义了由孤立的反射点组成的一类框架。这类框架的混合逻辑与经典命题逻辑几乎没有区别，并且是NP-完全的。 另一方面，正如我们正如这个例子所表明的那样，同一个公理在两种语义中可能有非常不同的效果，这些不同可以影响证明理论和结果逻辑的计算复杂性。 类似地，定义T0空间的更复杂的公式在关系语义学中具有非常不同的含义：定义了反对称框架类尽管有这些困难，但仍有可能用关系术语来简化拓扑逻辑Log（ T0）和Log（T1），而且实际上我们所有的后续工作都依赖于这种简化。特别地，Sustretov [14]证明了这些逻辑对于满足某些额外条件的有限传递和自反关系模型这些条件是：定义2.4（关系模型条件）T0不存在包含由名素命名的点的非平凡圈T1由名词命名的点除了来自自身之外没有传入弧D. Sustretov等人/理论计算机科学电子笔记231（2009）309313⊆∀ ∃∃∈ ∈∈∃∃∀Sustretov [14]使用这种简化来表明这些Log（T0）和Log（T1）都是PSPACE完全的。这些是我们将进行第一个拓扑定理证明实验的逻辑。我们将研究两种方法，这两种方法都依赖于Sustretov的关系表征。在第一个实验中，我们将直接实现Sustretov的PSPACE算法。在第二种情况下，我们将借助通用模态来验证刚刚提到的框架类，然后将通用模态编码问题交给基于表格的证明器。3使用Hyloban进行在本节中，我们介绍HY LO BAN，这是[14]中开发的基于游戏的方法的概念验证实现。这个名字是对推箱子的暗示，这是一款最近被证明是PSPACE完整的游戏。 我们的证明者玩游戏是为了此外，由于它所处理的混合逻辑是PSPACE完备的，因此可以（理论上！）用我们的证明器玩推箱子。证明器的工作原理是在一个两人博弈中搜索获胜策略，我们将在下面介绍;这个博弈有两个变体：一个是T0，另一个是T1。 证明这个博弈中获胜策略的存在等价于在[14]中给出了满足T0（或T1 这个游戏是通过在棋盘上放置一个叫做Hintikka集的结构来进行的 并通过某种关系将它们联系起来定义3.1（Hintikka集）设F是在子公式和单否定下封闭的公式集（从现在开始，我们将在子公式和单否定下封闭的公式集Γ表示为Cl（Γ））。 集合A如果它是满足以下条件的极大子集，则称之为Hintikka集：(i) ∈/A(ii) 如果∈∈Ai∈/A(iii) 如果∈，则∈Ai ∈A且 ∈A有两名球员：贝拉尔（男）和露易丝（女）。Loise通过将Hintikka集放在棋盘上并在其上定义传递自反关系R阿贝拉尔介绍了她必须面对的挑战。 她在比赛开始时集合{X0，...，Xk}在板上。集合必须满足以下条件：（ROOT）（INIT-NOM）（INIT-UNIV）（INIT-CYCLES）X0包含k，k≤|氯（氯）|、每个标称出现在一个Hintikka集合中对于所有的Xl和所有的Eχ Cl（n），对于某个j，Eχ X l i ∈Xj，R没有非平凡圈[对于T1博弈]。如果条件不成立，洛伊丝立即输了。 belard314D. Sustretov等人/理论计算机科学电子笔记231（2009）309∃∈∀∃∃∀∃∃∀∀∃∀∃（钻石）（UNIV）（名义）（循环次数）（无-收到）对于所有的Qχ∈Cl（λ），如果Qχ∈/Xl，则Qχ∈/Y和χ∈/Y，对所有的Xl和对所有的Eχ∈Cl（n），Eχ∈Xli <$χ ∈Xj，对某些J如果i Y对于某个名义i，那么Y是在第一步中使用的Hintikka集合之一。如果是这种情况，游戏停止，她赢了（除非下一个规则被违反，在这种情况下，她输了），R没有包含Hintikka集合的循环，这些集合包含不同的名词[对于T0游戏]。由名词命名的点除了来自自身之外没有传入弧[对于T1游戏]，如果Loise不能找到一个满足这些条件的Y，那么游戏停止，Belard获胜。否则，贝拉尔必须从最后一组（即Y）中选择一个形式为Q的公式，游戏以类似的方式继续进行。如果洛伊丝能够应付贝拉尔的所有这并不能保证游戏会在某个时刻停止，所以我们引入了一个额外的规则。 一个公式列表， 如果他第二次玩一个公式，loise必须用与他第一次玩公式时如果她的集合满足上一段的条件，Loise就赢了;否则，她就输了。游戏立即停止。我们在上一节中看到的游戏HY LO BAN的实现是用函数式语言Haskell [10]实现的，使用Glasgow Haskell编译器（GHC）[7]。 该代码在GNU GPL下发布，可以从www.example.com下载http://trac.loria.fr/projects/hyloban。除了算法的主循环（这是极大极小的一个实例）之外，实现的最重要部分是生成Hintikka集。每转一圈，loise把Hintikka集放在黑板上，使其服从某些条件。这意味着实现应该包括生成满足给定条件的Hintikka集我们当前的实现在游戏开始时从输入公式生成所有可能的Hintikka集。在博弈过程中，当我们需要满足特定条件的Hintikka集时，我们扫描生成的Hintikka集并过滤好的Hintikka集。让我们看看这是如何发生的。3.0.1Eloise在她的第一个回合， 洛伊丝的自然策略是尽量少放一些辛提卡集尽可能在董事会上，以减少贝拉尔找到一个挑战，将使她失去的机会。因此，我们的实现尝试生成尽可能小的初始板。必须由Hintikka集满足的条件放在、D. Sustretov等人/理论计算机科学电子笔记231（2009）309315∈¬∨¬∈∀∃第一回合的比赛如下：- 至少一个公式必须包含输入公式，- 在输入公式中出现的每一个名词都应该属于某个集合。对于每个公式E Cl（φ），（INIT-UNIV）条件留下两种可能性，导致其自身的条件：- E1属于一个Hintikka集合，E 1应该属于所有生成的Hintikka集合（让我们假设E1存在），- E1和E2不应该属于任何生成的Hintikka集合（E1普遍存在）。可以注意到，某些条件对所有生成的Hintikka有影响，而某些条件只涉及单个Hintikka集。如果我们想生成所有可能的Hintikka集，我们应该考虑第二类条件的所有组合。由于每个条件都应该至少有一个Hintikka集满足，因此使用以下方法似乎是合理的。 我们生成所有条件的集合的所有可能的分区。 一个划分的每个等价类对应一个Hintikka满足这个类的条件的集合例如，考虑公式= i j。 我们有三个条件与这个公式相关联：i应该出现在某处，j应该出现在某处，j应该出现在某处。可能的分区有：我|J |i，j|吉吉|j，i，|ji，j，在我们的实现中，我们使用[12]中描述的技术生成条件的所有分区。对于每个生成的划分，我们遍历它的等价类，并为每个等价类生成满足该类中条件的所有Hintikka集。然后，将满足不同等价类的条件集的Hintikka集放在一起，以形成候选初始板。然后，对于每个生成的初始棋盘，检查所有“全局”条件（例如，不存在属于几个不同Hintikka集的标称），以确保它是良构的。存在公式被分开处理。在生成parti- tions之前，我们从Cl（n）中遍历形式E的所有公式，并确定每个公式其中，是否存在性地发生或普遍地发生在第一在这种情况下，我们得到一个参与分区生成的“单独”条件，在另一种情况下，我们有两个全局条件。然后，我们如上所述生成分区和初始板。对所有可能的故障出现类型组合重复此过程。3.0.2埃洛伊塞的 后续匝数当贝拉尔在黑板上写下一个公式时，欣蒂卡设定， 卢瓦兹普特 答案必须包含“否”。 它也必须不包含任何E Cl（）的，并且存在一个不包含E的Hintikka集。316D. Sustretov等人/理论计算机科学电子笔记231（2009）309∀∃∀∃当belard重复使用一个公式时，loise必须用她第一次回答公式时所用的同一个Hintikka集来回答。因此，不存在要生成的Hintikka集合。我们保持一个地图之间的公式放在董事会上的贝拉尔，和Hintikka集回答他们每一个露易丝，我们要找回这已经让欣蒂卡从那里开始了3.1结构HY LO BAN使用一个全局状态，其中主数据结构是BoardData，它包含一个Board对象，输入公式的非负子公式闭包和输入公式的所有可能的Hintikka集合的集合。Board对象的特点：• hSets：：[HintikkaSet]Hintikka在板上设置。列表中的顺序很重要。列表的尾部是最新的Hintikka集。• ：：Matrix表示Hintikka集之间的R关系。我们不强制R的自反性和传递性，但我们扩展了DIAMOND条件来检查自反一致性。• firstHSets：：[Int]第一个Hintikka集合的有序索引（在输入公式的所有可能的Hintikka集合中）放在黑板上这是董事会的一个散列• forcedFormulas：：[公式]必须存在于所有Hintikka集合中的公式。 对于每个公式E（E），[2019 - 05 - 19][2019 - 05][2019-0我们将马上看到我们如何使用这个对象的某些部分来实现基本的优化。3.2缓存初始板的生成程序可以两次生成相同的板。考虑前面例子中的两个分区i，|J我|j，从两个分区开始，可以生成以下初始板：{{i，}，{j，}}。为了解决这个问题，我们使用缓存。对于每个输入公式，Cl（n）是固定的，所有可能的Hintikka集合的集合也是固定的。因此，我们可以将每个Hintikka集合关联到一个整数。这就是我们在Board对象的第一个HSets字段中所做的。因此，每个初始棋盘都由Hintikka集合索引列表按递增顺序标识。我们存储已经考虑过的每个初始棋盘的哈希值，以避免分析同一个游戏两次。我们进行的测试表明，缓存的影响目前几乎D. Sustretov等人/理论计算机科学电子笔记231（2009）309317→微不足道。尽管如此，在证明器中存在这个开关可以为更聪明的优化铺平道路。4使用HyLoTab进行在HY LO BAN中体现的基于博弈的拓扑定理证明方法使用了Sustretov但是，正如Balder ten Cate所观察到的，有一种更简单的方法可以利用Sustretov让首先 考虑一个含有名值的公式φi1，.，我知道。 那么这个公式Kφ1（φ）=φ<$ A（Qik→ik）i=1在有限关系S4模型上是可满足的，如果这个模型满足定义2.4中的条件T1，对于所有出现在φ中的名词。毕竟，A（Qikik）是T1条件的直接陈述：它清楚地断言（对于每个出现的标称 在φ中），所有由名素命名的点除了来自自身之外没有传入弧。因此，我们已经使用了通用模态来全局地强制模型上所需的约束。对于Log（T0）来说，事情几乎同样简单。设Nom（φ）为φ中的名素集。然后公式：0（φ）=φi，j∈Nom（φ）@i<$j→（@iQ<$j@jQ<$i）在有限关系S4模型上是可满足的，如果这个模型满足定义2.4中的条件T0，对于φ中出现的所有名词对。毕竟，这些对上的合取系统地排除了涉及由这些名词命名的点的非平凡循环。 我们再一次使用了普遍模态在模型上全局强制所需的约束（回想一下，@是使用 通用模式）。因此，下列命题成立：提案4.1• 在S4框架类上，一个属于Log（T0）i →φ（φ）的公式φ成立.• 在S4框架类上，一个属于Log（T1）i→φ的公式φ成立.这给了我们什么？首先，现在有一个更简单的证明，证明T0和T1的逻辑的PSPACE完备性。 毕竟，在富含泛模态的混合逻辑中，S4框架的逻辑已知是PSPACE完全的（参见[3]），并且我们刚刚在该逻辑中编码了T0和T1有效性318D. Sustretov等人/理论计算机科学电子笔记231（2009）309V = 2，N = 2，R = 1，D = 1，L =[1.]五、1001010.10 2 4 6部分条文图1.在HY LO BAN和HY LO TAB之间，对于具有T0公理的SAT测试，中位时间与公式大小然而，更重要的是，它为我们提供了一种新的混合拓扑定理证明方法。给定一个可以处理S4和通用模态的混合逻辑证明器，前面的命题给出了一个简单的配方使用它的拓扑定理证明目的。幸运的是，这样一个证明者是存在的，即HY LOTAB[16];事实上，目前HY LO TAB是唯一这样的证明者。因此，有了HY LO TAB，我们就有了第二种证明拓扑定理的方法，可以与HY LO BAN进行比较。5绩效评价现在让我们评估这两种方法的性能。 实施后 最后一节的T0和T1满意度测试到HY LOTAB中，我们比较了它到HY LO BAN，我们得到了图1中具有T0公理的 而图2则是具有T0公理的公式本测试确认， 目前，HYLO BAN正在进行初步研究-泌尿系统。尽管与HY LO TAB相反，我们可以保证证明器的终止，但它的平均执行时间要高得多。 我们已识别HY LO BAN在表现方面的两个主要弱点• Hintikka集• Hintikka集请求第一点可以大大改进。目前，我们将输入公式的所有Hintikka集的集合表示为列表，这使得扫描Hintikka集的操作非常昂贵。 解决这个问题的方法是存储所有Hintikka的集合集合作为一个二叉树，其中每个分支代表一个可能的Hintikka集合（见图3的例子）。 距离树的根为n的节点表示Cl（n）的所有正公式列表中的第n个左（或左）右）输出边表示包括该公式的选择（分别hylobanT0hylotabT0中位用户执行时间D. Sustretov等人/理论计算机科学电子笔记231（2009）309319∪V = 2，N = 2，R = 1，D = 1，L =[1.]五、1001010.10 2 4 6部分条文图2.在HYLO BAN和HYLO TAB之间，对于具有T1公理的SAT测试，中值时间与公式大小图3. <$（Qp）~ p的可能Hintikka集的树表示其否定）在Hintikka集合中。一个不在根的距离n+1处的叶子意味着在其分支中所做的选择不可能有Hintikka集这种表示比所有Hintikka集合的列表占用的空间少得多，并且查询它，即回答问题这将是一个不那么复杂的操作。对于第二点，我们想在Hintikka集合请求上添加约束目前，我们想要生成一个包含公式的Hintikka集合。相反，我们可以请求所有包含csq（n）的Hintikka集，其中csq（n）是通过在公式n上运行一个简化的tableaux算法而获得的一组这些结果公式将是存在于tableaux算法的分支中的公式集合，而不使用分支规则。由于我们手头有我们需要的东西，我们将把HTAB[9]中的一些源代码合并到HY LO B最后一个优化是重新使用辅助tableaux算法的思想，以删除在混合逻辑的较弱公理化中已经不满足的输入公式部分。 例如，如果输入公式是和，并且如果我们可以证明在混合逻辑的较弱公理化中是不可满足的，那么我们可以在上启动基于游戏的证明器。hylobanT1中位用户执行时间320D. Sustretov等人/理论计算机科学电子笔记231（2009）3096结论本文讨论了定理证明中的两个初步实验 拓扑混合逻辑;这些实验的长期目标是将这样的定理证明集成到IN TO HY LO[2]框架中。正如评估清楚地表明，当前版本的基于游戏的方法在HY LO BAN中实施的基于表格的方法显然不如使用通用模式的基于表格的方法。但我们认为，值得进一步试验基于游戏的方法。首先，我们已经看到，有一些明显的优化可以内置到系统中。 此外，H Y L O B AN本质上是一个通用的基于博弈的定理证明工具。我们认为，这样一个工具可以是对信息技术框架的有益补充。 例如，我们相信它可能对混合邻域逻辑的定理证明实验有用（参见参考Diego关于这种逻辑的一些初步工作）。尽管如此，目前更好的拓扑混合定理证明器的最佳选择在于基于表格的方法。很明显，这种方法的性能可以大大提高。特别是，HTAB的第一个版本，一个用于混合逻辑的终止tableau证明器最近已经实现（见[8，9]）。这个新的证明器令人信服地优于HY LO TAB的基本逻辑K，我们相信它将是简单的，以纳入HY LO TAB最近宣布的终止tableaux算法，其中包括混合S4丰富的通用模态（见[5]）。这似乎可能导致大量的性能增益，并希望运行HT实验室为基础的拓扑定理证明不久。引用[1] M. Aiello，J. van Bentham，and G.别扎尼什维利关于空间的推理：模态方法。Journal of Logic andComputation，13（6）：889[2] C. 阿雷斯山口 Bla ckburn，D. Go r'ın，andG. 霍曼。混合逻辑的推理工具（InToHyLo）。Mandarpt，LORIA，可从http://www.loria.fr/ com-areces获得，2007年。[3] C. Areces，P. Blackburn，and M.马克思混合时态逻辑的计算复杂性。Logic Journal of the IGPL，8（5）：653[4] P·布莱克本表示、推理与关系结构：混合逻辑宣言。Logic Journal of the IGPL，8（3）：339[5] T. Bolander和P. Blackburn。扩展K的混合逻辑的终止表演算。提交给《模式方法》，2007年。[6] L. 艾 萨 基 亚对 角 构 造 ， Lüob的穆拉，和Cantor的散布空间。 在 语言 学 和 语 义 学 研 究 ， 第 128-143 页 。Metsniereba，1981年。用俄语[7] GHC，格拉斯哥哈斯克尔啤酒厂。http://www.haskell.org/ghc/网站。最后访问时间：2007年9月15日。[8] G. 霍曼。 H Ta b：用于混合逻辑的终端表格系统。 硕士论文，D ′ eparteme n t de formation d o ctorale eninformatique，UFR STMIA。洛林高等教育学院，2007年。（英文版）。[9] G. Ho Mushmann和C. 槟榔。HTab：一个用于混合逻辑的终端表格系统。提交《模式方法》，2007年。[10] S. Peyton Jones and J. Hughes （ editors ） . Haskell 98 ： 一 种 非 严 格 的 纯 函 数 式 语 言 。 技 术 报 告 ，Haskell.org，1999年。D. Sustretov等人/理论计算机科学电子笔记231（2009）309321[11] J. McKinsey和A.塔斯基拓扑学拓扑学的代数Annals of Mathematics，45：141[12] M. 奥洛夫有效生成集合划分。技术报告，乌尔姆大学工程与计算机科学学院，2002年http://www.cs.bgu.ac.il/。[13] 诉谢特曼实平面域的模态逻辑Studia Logica，42：63[14] D. 苏斯特雷托夫 拓扑语义和可判定性。http://www.arxiv.org/abs/math/0703106网站。[15] A. 塔斯基这位老人说的话和他的逻辑是一致的. Fund. 数学，31：103-134，1938.[16] J. 范艾克。HyLoTab-基于表格的混合逻辑定理证明Mandarin pt，CWI，可从http://www.cwi.nl/ ~jve/hylotab获得，2002年。