《证明规划与推理技术的认知充分性》- 电子科学笔记58卷第2期(2001年)

《理论计算机科学电子札记》58卷第2期（2001年）网址：http://www.elsevier.nl/locate/entcs/volume58.html14页基于索引公式Serge Autexier1FR 6.2 Informatik，萨尔大学P.O. Box15 1150， 66041Saarbrucken，德国摘要证明规划的一个主要动机是弥合高层次的差距，认知充分推理的特定领域，和演算级推理，以确保健全。对于高推理水平，表征和推理技术的认知充分性是一个主要问题，而对于低推理水平，充分性是一个主要问题。建模域是重要的。 此外，论证工作是一项工程任务，需要支持设计和应用论证-搜索工程方法。为此，我们提出了一个框架，显式地支持不同的推理水平。为了构建推理层次，框架允许抽象和证明搜索的保留技术的显式表示。为了确保合理的推理水平内，我们使用的技术依赖于索引公式的概念矩阵表征的背景下开发的。此外，我们引入了一个统一的概念，上下文reasoning，并勾勒出基本的战术定义的战术组织内部和跨不同的推理水平的整体证明搜索。关键词：证明计划，方法论，抽象，矩阵表征1引言证明规划的一个主要动机是一方面允许高层次的推理，这是（认知）足够的具体问题和领域。另一方面，推理过程的最终产物必须是一个微积分级别的证明。一些逻辑，为了有一个真正健全的证明。除了认知动机外，另一个原因是对某个定理的证明是一个工程任务。类似于软件开发，在软件开发中，一个人从一个程序的高级规范开始，然后重新定义，1 电子邮件地址：Autexier@ags.uni-sb.dec 2001年由Elsevier Science B出版。诉 在CC BY-NC-ND许可下开放访问。奥特希耶2在某些目标编程语言的可执行程序中，我们将证明计划视为设计（并随后应用）不同推理水平的方法以及逐步重新证明规范（即证明计划）的方法。因此，证明计划已被引入作为一种方法，将定理的高级证明计划重新提升到微积分水平。不同推理水平的目标是不同的：对于高推理水平，表示和推理技术的充分性虽然一个推理层次内的推理应该是合理的，但由于存在不同的推理层次，因此存在另一种相对合理的概念。高水平的推理是相对合理的。一些较低的推理水平，如果有任何高级别的证明可以被称为一些低级别的证明。通常，这种相对可靠性并不成立，这是抽象存在时的一个众所周知的现象[5]。我们不想强制要求高推理水平的相对可靠性，因为这通常会妨碍表示的充分性，而这些水平的主要目的是允许对证明计划进行有效和充分的搜索。一个高推理水平上的证明的相对可靠性是通过逐步将这个证明转化为一个微积分水平的证明来建立的。在较低的推理水平上，我们不太关心表征的认知充分性，而是关心wrt的充分性。建模域，例如一些程序行为或数学域。在本文中，我们提出了一个证明规划框架，支持设计和应用的证明搜索工程方法。首先，我们在第二节中定义了推理层次的概念，它由推理对象（如公式、序列等）组成。和推理过程（例如，策略、规划算法、一般定理证明算法等）。例如，在像[10，2]这样的证明规划器中，推理对象是序列以及某些方法的前置和后置条件，它们被用作推理规则。证明规划器的推理过程是应用这些方法的深度搜索算法以确保wrt的正确性在一个推理层中的一些逻辑为了表示的充分性，逻辑不嵌入在某些元逻辑中。相反，我们在第4节中介绍了在矩阵特征化[12，9]的背景下开发的依赖于索引公式概念的技术。这些允许一个大类的经典，模态和直觉逻辑的统一处理，而不必改变公式的语法其次，我们在第三节中定义了垂直结构机制，不同的推理水平。这一方面包括抽象的明确定义，它定义了较高推理层次的推理对象如何另一方面，我们引入了元素的概念，它决定了如何更高层次的推理过程可以实现一些较低层次的推理过程。这包括奥特希耶3例如编码在证明计划器方法中的元素的概念，如[10，2]，其中方法内部包装的策略决定了由方法的前置条件和后置条件描述的抽象规则的元素。基于一般的元素概念，抽象证明的元素可以用一种统一的方式定义。第三，推理过程应该以直观的方式来定义，这也是因为认知充分性的总体动机。为此，我们在第5节中介绍了窗口推理推理，这是一种直观推理风格的形式化，它允许将推理集中在子公式和子项上，并旨在进行上下文推理。我们将窗口推理推理与第4节中的索引公式相结合，并将其作为一个副产品来介绍如何以规范的方式进行上下文推理。最后，我们将在第6节中介绍基本的编程语言来定义推理和推理过程，以及如何将它们结合起来，以组织整体的证明搜索。这些建立在由窗口推理推理提供的直观推理规则的基础上，并且具有明确的失败和成功语义。2推理水平在本节中，我们介绍推理层次的概念。这些都是横向结构的框架，反对抽象和renement技术（cf。（3）垂直结构。一个推理层次一方面由我们想要推理的对象以及基本推理规则组成，另一方面由在一个推理层次内组织证明搜索的推理过程组成。前者由一个签名和一组公式wrt定义一些逻辑。因此，推理层次的推理对象和规则由一个对（;）给出，其中是签名，是一组\公理”，我们将这样的一个对表示为表示。这类似于形式规格说明语言中的规格说明的概念[8]，例如，用于定义抽象数据库和关于抽象数据库的函数对于一个推理层次，签名决定了推理对象的语法，可用的基本推理规则由公理”from“决定。示例2.1作为示例，我们给出了TLA公式[7]的TLA表示和TLA公式抽象的TLA-状态&跃迁表示。TLA的签名包含通常的逻辑连接类型，以及2;3，并且还包含WF以表达公平性要求。作为一个例子，我们使用一个简单的程序，它有一个初始值为15的计数器x并且如果计数器大于0，则在每一步中减小该计数器这是在TLA中由以下公式x=15^2（ x0^ x0 =x 1）^WF（x 0^x0 =x 1）x为了证明计数器最终具有值0（由奥特希耶43x= 0），我们使用由状态和状态转换组成的表示作为抽象。 这种表示被称为&TLA-StatesTransitions，由表示状态的状态hni（其中x的值为n）和由8 n表示的状态转换组成：hni）hn 1 i。 这是对程序所做的转换的抽象，即：x0^x0 =x1。 找到3x = 0的proof-plan，包括在（抽象）表示TLA-States&跃迁上证明h 0 i。2推理层次的第二个组成部分是推理过程，它在推理层次内组织证明搜索我们对推理过程采用了一种通用的概念，将其定义为某种编程语言中的算法，通过应用基本推理规则与证明交互此外，推理过程带有成功和失败的概念，以反映自己的行为。例如，在失败的情况下，推理过程可能会调用回溯到以前的某个证明状态。推理过程的这个概念是足够普遍的，以涵盖在自动定理证明中开发的各种特定推理过程，例如，战术定理证明器中的战术，自动定理证明器中的各种算法，或者某些证明规划器中的证明规划算法总之，我们已经定义了一个推理级别，由两部分组成，即表示定义的推理对象的语法和reasoning程序，以组织推理级别内的证明搜索。这可以通过以下等式来描述：推理水平=表征+推理过程下一步是建立推理层次。为此，下一节将介绍垂直结构，描述在推理级别之间切换的机制3构建推理层次在本节中，我们定义了构建框架的不同推理层次的机制（参见。图1）。垂直结构有两个双重概念：第一，抽象可以被定义为描述如何从较低推理水平的对象构造较高推理水平形式上，抽象是源表示RS的一组对象到某个目标表示RT的一组对象的映射。为了框架的目的，我们定义了一个抽象，包括名称，源和目标表示RS和RT，以及计算映射的抽象过程示例3.1将自然数和标记片段的源表示NAT（LF-NAT）视为相应的目标表示作为示例。奥特希耶5推理水平3 =表征-3+推理过程3抽象关系推理水平2 =表征-2+推理过程2抽象关系推理水平1 =表征-1+推理过程1Fig. 1. 构建推理层次站。标记片段是归纳定理证明的上下文中已知的抽象，其中它们用于在共享公共骨架的两个项之间的特定差异（所谓的波前）上进行抽象。表示NAT由自然数的签名和定义自然数加法的两个公理（1）8年 0+ y = y（2）8x; ys（x）+ y =s（x + y）该表示LF-NAT一方面由通过函数扩展NAT的签名的签名组成：Nat！Nat，用于表示波前，另一方面是公理（3）8y（y）= y（4）8x; y（x）+ y =（x+ y）（5）8x（s（x））=s（（x））标记片段抽象是从NAT到LF-NAT的抽象，其相关抽象过程将单例f（1）g映射到单例f（3）g，并将单例f（2）g映射到集合f（4）;（5）g。2因此，抽象由源表示和目标表示以及将对象从源表示映射到目标表示的函数组成。这可以通过以下等式以直观的方式表示：抽象=源目标表示+抽象过程双重垂直结构化机制是更高层次的结构化推理程序到较低层次的推理程序。 举个例子高级推理程序的一些规划算法，它从方法中计算证明计划。该证明计划是证明计划过程的推理层上的“证明”，并且包括由方法的前置条件和后置条件定义的基本重写规则的应用我们可以将这个规划过程与一个执行过程相关联，该过程采用生成的证明计划，并通过调用不同方法中的策略来执行它 在这种情况下，付款信息与奥特希耶6通过该方法对较高推理层次的每个基本推理规则进行推理。一个方法描述了一个抽象的证明步骤满足一定的模式（由方法的前置条件和后置条件描述），可以通过方法内部包装的策略来修正过程利用这些知识来修正证明计划。一般来说，不可能通过模式来描述这种关系信息。为了处理一般情况，我们允许将一个推理过程与某个推理过程联系起来。 这样的推理过程将推理过程生成的证明作为证明计划来计算较低推理级别上的证明（使用较低级别的推理过程）。 与推理过程类似，推理过程带有明确的成功和失败语义来反映它们自己的行为。例如，这允许回溯重置过程并尝试替代重置。从上面我们可以通过陈述一个推理过程和一个相关的推理过程来总结推理的概念。这可以通过以下等式来描述推理=推理过程+推理过程请注意，某个推理过程P的推理过程可以双重地解释为某种抽象，其中推理过程所使用的所有（较低级别）推理过程都被抽象为推理过程P。这种抽象的概念与上面提出的概念不同，因为它是推理过程的抽象，而前者是对象和公理的抽象。此外，执行过程在执行期间利用关于对象抽象的知识。因此，一个对象抽象也产生了一些元素的概念。 我们之所以主要为对象引入抽象，为推理过程引入抽象，是因为这是它们的常用方式。4处理可靠性在本节中，我们定义了一个统一的机制来处理各种逻辑的可靠性。为了表示的充分性，我们希望直接支持wrt的可靠性一些逻辑而不改变公式的语法因此，我们不想在一些元逻辑中嵌入一个逻辑，例如。直觉高阶逻辑在比较的代表介绍了在节。2.逻辑也定义推理对象的语法，但有自己的形式证明理论（而表示是相对于某个逻辑的，因此从这个逻辑“继承”证明理论因此，它的证明理论决定了，例如，在这个逻辑的微积分中，某个对象级量化器的消除规则是否必须满足本征变量条件，或者在某些模态逻辑中，一个对象级量化器的其他部分如何被某个2或3奥特希耶701010（c）0（_）+ '++（））+ '+（^）的方'（^ ）+'++（_ ）的方'（8x'）（'[x=c]（2'）'图二. 带符号公式处理不同逻辑的证明理论的后台机制必须允许对这些逻辑的可靠性和完整性结果进行统一处理。命题逻辑和一阶逻辑、经典逻辑、模态逻辑和直觉逻辑的基础由索引公式树[12]提供，并依赖于（子）公式的极性和统一符号[12，4，3]。统一记法的出发点是有符号公式的概念，对于公式，用某些命题（“+”）或命题（“）来注释。直觉上，有符号公式“+”出现在“+”的后继项中，即“和”出现在一个词的先行词中，即 ;“”。有符号公式可以根据它们在证明搜索过程中的行为分为不同的类：''_。 相应的分解规则的应用导致单个的"“;。所有这些类型的有符号公式都被称为类型。这种类型的有符号公式的完整列表在图中的表中给出二、此外，那些有符号公式的分解导致分裂的证明树被称为是类型（cf。图2）。类型的带符号公式对应于实例化规则，而不限制被替换项，而对于带 符 号 的 类型p，实 例 化 规 则 必 须 考 虑 特征变量条件（例如，（8x'）+，相当于“8x”）。对于模态逻辑公式，-型有符号公式的分解不影响子图中的其他公式（如2“”），而-型有符号公式的分解改变子图的其他部分（如2“”）。“2”;）。在图2中，规则还指示极性如何被继承到有符号公式的子公式。使用这些规则，极性可以被分配给公式的所有子公式，并且子表达式的极性指示该子公式是否将出现在子表达式的前件或后件中，如果所有结构子表达式分解规则被应用直到该子表达式。 例如mula（'）的签名 对应于;'）`。- 规则将这个有符号公式简化为有符号公式的+和。第0（c）段Æ0（8x'）+（'[x=c]（2'）'+奥特希耶8一一一a0级a1a4a2a5a3a6a70 03 6808图三. 索引公式树这对应于如果在;'）'上应用）-L有效分解规则所发生的情况，因为它导致证明的分裂（由指示），并且'发生在第一个前提的后继项中';，并且发生在第二个前提的先行项中;'。[12]中介绍的索引公式树利用公式的树结构，并根据具有各自极性和统一类型的归约规则来注释每个子公式。考虑图中的索引公式树。3的签名为穆拉（（28xP（x）（9年（P（y）^2P（y）+。对于每个子公式，都有一个位置ai，它要么是位置常数，要么是位置变量（上划线，如①的人。一组关联每个位置都在相邻的表格中列出：这些是实际的子。公式（称为位置的标签）、其极性、其统一类型（称为主类型）和其辅助类型（父公式归约规则中的类型）。根据这些归约规则，只有通过类型位置相关的子公式才可以一起出现在一个最终表达式中（在应用相应的微积分分解规则之后）。这可以通过由位置α 0相关的子公式8x P（x）和P（y）来说明，或者类似地，通过子公式8xP（x）和2P（y）来说明。因此，从索引公式树中，我们获得了一些子表达式的上下文的简单概念，即有符号公式树的那些部分，其可以是\used”用于此子表达式。这在第5节中被用来处理上下文推理。索引公式树的树结构引起位置之间的排序。一阶替换实例化绑定在一一uPol（u）实验室（u）Ptype（u）S型（u）a0级的1一个2一个3a0级3一个4一个5一个6a0级6a0级8+Æ+++++公司简介（2（8xP（x）8xP（x）P（y）1002奥特希耶9一些位置a的主要类型，并导致一个额外的排序关系之间的位置a和-或非-类型的位置绑定变量，（十）. 与原始订单相结合，我们得到一个关系. 这样的一阶代换只有在以下情况下才是合理的：是不需要的。此外，我们可以将任何位置a与一串位置相关联，这些位置由一些控制a的位置组成（即较小的wrt。 ），并且是主要类型或。 这样的字符串称为位置a的模态前缀x。在pre x中实际使用哪些位置取决于所考虑的模态逻辑（K、K4、S4等，参见[12]详情。变量位置是所有主要类型的位置。模态替换用于通过模态位置字符串实例化位置变量。取决于所考虑的模态逻辑，存在如何实例化位置变量的一组限制（参见图1）。[12]）。此外，类似于第一阶替换模态替换诱导了- 还有- 类型的位置，并再次诱导整体排序必须我很渴望。所有关于变量的实例化、位置变量、位置之间的诱导全序的不自反性的要求都包含在L-容许替换的统一概念中，其中L是经典的一阶逻辑，或命题或一阶模态逻辑K，K4，D，D4，T，S4，或命题或一阶直觉逻辑。L-容许替换的统一概念是统一处理一大类逻辑的关键概念。基于这些技术，我们引入了有效证明状态的统一概念（即，具有不规则排序的带符号公式树）。 从[12]中我们得到，应用L-容许替换保持了证明状态的有效性。计算L-容许替换的问题可以通过使用带有对象变量的发生检查的标准union过程和来自[9]的仅计算位置变量的L-容许替换的一般预union过程来解决，其中L是上述逻辑中的任一个。有效证明状态的概念随后可以用来正式证明我们可能在有符号公式树上定义的任何其他变换的L-可靠性。因此，使用带符号的公式树为我们提供了一个强大而统一的机制来支持框架内的各种逻辑。5直觉和上下文推理对于推理和检索过程的设计，我们支持一种直观的推理风格。为此，我们的目标是把推理过程集中在一些实际表达式的任意子表达式上，并在焦点内得到上下文推理的有力支持。窗口推理[11，6]已经被引入作为一种直观和层次推理风格的形式化。基本对象是窗户h[]`P（a））：（a=b）i+奥特希耶10wwWWwwW其表示焦点在正（+）公式P（a））：（a= b）（表示为窗口的内容）上，并且该焦点的上下文为空（[]）。基本的窗口推理规则是(i) 聚焦于窗口h[]`P（a））：（a=b）i+h[a=b]`P（a）ih[a=b]`ain;哪里表示焦点导出步骤。 请注意，这条规则必须是-ned用于示例中的任何逻辑连接词（正）和示例中的参数位置（的第一个参数），以便以一致的方式调整上下文。虽然这对于经典逻辑来说并不困难，因为在经典逻辑中，子焦点的上下文要么相等，要么是前一个上下文的扩展，但一旦我们处理非经典逻辑，这就变得困难了(ii) 使用来自上下文的信息转换窗口的内容h[a=b]`aih[a=b]`bi;(iii) 离开一个焦点并返回到父焦点h[a=b]`bih[a=b]`P（b）ih[]`P（b））：（a=b）i+：此外，窗口推断推理还允许关注窗口的条件。在这组基本规则中，我们添加了一条通用规则，以便引入案例分析：h[H]`tiph[Aj H]`tip和 h[Bj H]`tip;为了确保案例分析2的可靠性，生成条件h[H]` A_ Bi+作为附加目标。为了允许一个直观的设计推理过程，我们集成了窗口推理推理与索引公式树（cf.秒4）通过用窗口注释索引公式树中的位置。由于关注子表达式是沿着树结构的，因此打开子窗口对应于在相应位置上添加窗口。类似地，离开焦点意味着从某个位置移除窗口并返回到先前的位置。将索引公式树与窗口相结合，得到了如下的框架结构：在框架内部，证明状态由带窗口的索引公式树表示。它们充当管理任何证明转换的可靠骨干，例如变量的实例化或来自上下文的规则的应用。被索引的公式树对推理过程是不可见的，推理过程通过注释到特定位置的窗口和应用窗口推断规则与它们通信，这导致证明状态的改变。 例如打开子窗口、实例化变量等。我的痛苦-2 即使是直觉逻辑。奥特希耶11Culty仍然认为，必须向推理过程提供上下文信息，例如窗口的极性是什么，哪些是可实例化变量，特别是哪些是来自窗口上下文的可能规则这些困难通过使用索引公式树来优雅地解决：窗口的极性：窗口的极性就是它在索引公式树中所处位置的极性。可实例化变量：某些窗口的可实例化为了检验一个变量的实例化的容许性，我们检验替换的L-容许性（即新的诱导序的不存在性，参见。秒4）.采样上下文规则：窗口的上下文由索引公式中的位置统一确定：索引公式的所有部分，通过类型位置与实际窗口相关，都在逻辑上下文中。事实上，根据图中的减少规则2、只有- 相关公式可能在某些情况下一起出现 在应用后的最终结果-使用相应的微积分分解规则（cf.秒4）. 因此，改变窗口内容的可用规则例如是上下文中的所有负方程和含义。负方程的应用基本上是一个调节规则，而负蕴涵的应用则这样一个规则的条件是所有与这个规则相关的公式。由此我们可以定义一个统一的 规 则u 的 概念！ V：当然，这个规则意味着如果我们提供条件，我们可以用V来替换风的一个常数。这个概念可以被正式定义，也可以被接受。焦点（即位置）。定义5.1 [容许替换规则]设a是某个索引公式树中标号s和极性p的位置。 然后你！ v是a的可容许替换规则，如果(i) u和v是负方程的左侧和右侧，即与a相关，或者u和v是分别具有极性p和p的相同模态或直觉预值的相关公式，并且- 与a有关，(ii) 和包含所有其他与u和v相关的公式。2替换规则的应用：要在某些焦点上应用替换规则，我们必须在语法上统一规则的左侧与焦点的上下文以及它们的模态前缀。此外，如果替换规则不是等式，则焦点和规则的左侧必须具有相反的极性。 对于uniation，我们使用对象级变量的标准uniation过程，并依赖于[9]中的通用预uniation过程，以便仅计算实际逻辑允许的替换。这允许证明所有逻辑奥特希耶12过程证明可达（窗口：TLA）抽象可达抽象窗口抽象证明可达结束过程精化抽象-证明-可达-精化抽象证明可达...末端精炼过程抽象证明可达（window：TLA-StatesTransitions）...见图4。在[12]中，TLA推理和修正程序考虑了替换规则应用的合理性。总之，窗口推理推理与索引公式的集成一方面允许设计直观的推理过程。另一方面，它提供了一个简单但强大的机制来支持上下文推理。6组织证明搜索框架内的整体证明搜索由推理和推理过程以及一些附加的语言结构来组织。推理过程基于窗口，并以两种方式与证明交互第二，他们可以在推理过程的任何阶段引入对一些任意公式A 1_：_An的案例分析。 遵循直觉推理范式，推理过程可以通过调用子窗口上的另一个推理过程来将证明搜索集中在某个子窗口上。最后，他们可以通过调用实际窗口的某个抽象上的推理过程来调用某个更高推理级别上的推理为此，它们指出了要使用的抽象和要调用的更高推理层次的推理过程在抽象推理过程成功的情况下，通过调用抽象推理过程的执行过程来完成（抽象）证明的执行只有在补救程序成功的情况下，证明计划尝试成功。例6.1以证明可达的推理过程为例，该推理过程专门用于证明形式3'的时间属性（参见图4）. 因此，推理过程的自变量被声明为来自表示TLA。此外，让抽象证明可达成为现实，奥特希耶13第二节中介绍的关于代表性TLA-国家&过渡的声音程序。 2，并让可达抽象是从表示TLA到表示TLA-States&转换的抽象。在图4中，我们描绘了证明可达的主体：该过程通过调用抽象来调用抽象推理过程，其将参数窗口抽象为表示TLA-States& Transitions并调用抽象推理过程abstract-prove-reachable。 如果这个过程成功，则调用相应的补充过程abstract-prove-reachable-refine，将TLA-状态&转换的抽象证明转化为TLA公式的证明。27结论在本文中，我们采取了动机，任务，以建立一个证明是一项工程任务。这就需要一种方法来设计和应用证明工程技术，我们强调，在证明规划中开发的技术在此基础上，我们开发了一个证明规划框架，它带有不同推理层次的明确概念。推理层次可以通过抽象和关系来构造。此外，我们强调，认知充分的推理是一个关键问题的设计更高的推理水平。这一方面要求不同推理层次的推理对象的表示必须是直观的。随后，一个统一的机制，以支持直接健全wrt。在不必改变逻辑公式的表示的情况下，已经引入了多种逻辑。此外，我们集成了这种机制与扩展的窗口推理推理风格，允许设计直观的推理程序。这种集成的一个主要好处是对上下文推理（直觉推理的一个关键概念）的直接而优雅的支持。最后，我们概述了如何证明搜索工程方法，如推理过程，抽象和RENNED的框架，以及如何将这些技术联系在一起，随后可以应用于证明搜索。该框架是INKA 5.0系统中核心推理机制持续实现的基础[1]。 未来的工作包括完成框架的实现，并通过实现特定领域和问题的推理层次和结构化机制来验证框架的充分性。未来的理论工作关注的是将进一步的逻辑整合到框架中。奥特希耶14引用[1] Serge Autexier，Dieter Hutter，Heiko Mantel，and Axel Schairer.系统描述：INKA 5.0 {逻辑旅行者。In H.陈文彬，《第十六届自动演绎国际会议论文集》，国立台湾大学出版社，1999年. 斯普林格。[2] 克 里 斯 托 夫 · 本 茨 姆Ller ， LassaadCheikhrouhou ， DetlefFehrer ，ArminFiedler，Xiarong Huang，Manfred Kerber，Michael Kohlhase，KarstenKonrad ， Erica Melis ， Andreas Meier ， Wolf Schaarschlinger ， JorgSiekmann，and Volker Sorge.mega：走向数学助理。In W.陈文辉，《第十四届自动演绎国际会议论文集》，北京：清华大学出版社，1997年.斯普林格。[3] M. 拟合一阶逻辑和自动定理证明/第二版。Springer-Verlag New York Inc.一九九六年。ISBN 0-387-94593-8。[4] 梅尔文·费丁模态逻辑的表法证明。Notre Dame Journal of Formal Logic，XIII：237{247，1972.[5] 福 斯 托 · 金 奇 格 里 亚 和 托 比 · 沃 尔 什抽 象 理 论 。Journal of Arti cialIntelligence，56（2-3）：323{390，1992。也作为技术报告IRST-技术报告9001-14。[6] 吉姆·格伦迪 HOL系统中的窗口推理。法律程序中HOL定理证明系统及其应用国际研讨会，1991年。[7] 莱 斯 利 · 兰 波 特 动 作 的 时 间 逻 辑 。 ACM Transactions on ProgrammingLanguages and Systems，16（3）：872{923，May 1994.[8] J. Loeckx ， H.- D. Ehrig 和 M Wolf 。 抽 象 数 据 类 型 的 定 义 。 Teubner ，Chichester;New York;Brisbane，1996.ISBN 3-519-02115-3。[9] Jens Otten和Christoph Kreitz。T弦统一：非经典证明方法中的统一前提。InP Miglioli，U Moscato，and et.例如，编辑，第五届研讨会论文集定理证明与分析表格和相关方法，LNAI 1071，第244页{260。Springer Verlag，1996年。[10] Julian D.C. Richardson，Alan Smaill，and Ian M.共享的系统描述：用-clam实现高阶逻辑的证明规划。在克劳德·基什内尔和Hel ene Kirchner，编辑 ， 第 15 届 自 动 演 绎 国 际 会 议 论 文 集 （ CADE-98 ） ， LNAI 1421 。Springer，1998年。[11] Peter D. Robinson和John Staples 形式化实用数学推理的层次结构。在Journal of Logic and Computation，第3卷，第47页{61，1993.[12] 林肯·沃伦非经典逻辑中的自动证明搜索：模态逻辑和直觉逻辑的有效矩阵证明方法。麻省理工学院出版社1990年《人工智能》系列丛书。