基于记忆的证明搜索的Elf程序的实验及其性能比较

110理论计算机科学电子笔记70第2期（2002）URL：http://www.elsevier.nl/locate/entcs/volume 70. html14页sLF中基于记忆的证明搜索：一个原型Brigitte Pientka1卡内基梅隆大学计算机科学系Pittsburgh，PA 15213，USA摘要Elf是一种通用元语言，用于以逻辑框架LF的风格指定和实现逻辑系统。在这个框架中的证明搜索是基于逻辑编程的操作语义。在本文中，我们讨论了一个原型的记忆为基础的证明搜索Elf程序的实验。我们使用两个应用程序比较了基于记忆的证明搜索，深度优先搜索和迭代深化搜索的性能：1）具有子类型和交集类型的双向这些实验表明，基于记忆的证明搜索是深度优先和迭代深化搜索的实用且总体上更有效的替代方案1介绍演绎系统通过公理和推理规则给出，在形式化程序的行为和提供程序行为的保证方面起着重要作用。在对“证明码”的研究在执行程序之前，主机可以通过检查程序的证书来快速验证代码几种验证代码的方法使用逻辑框架LF[6]作为指定安全策略的元语言。Appel和Festival [1]使用基于LF的高阶逻辑编程语言Elf[11]实现他们的安全策略为了验证给定的程序是否满足指定的安全策略，该规范由逻辑编程解释器执行。Necula和Rahul [8]使用基于LF子集的逻辑程序解释器来检查正确性1电子邮件：bp@cs.cmu.edu2002年由ElsevierScienceB. V. 操作访问根据C CB Y-NC-N D许可证进行。皮恩特卡111的证书。在他们的方法中，证书是一个比特串，它引导逻辑编程解释器在证明重建过程中解决不确定性选择使用LF等通用框架的一个主要好处是，它减少了每个特定策略所需的时间。通过对LF的一个逻辑程序设计解释的as-签名，我们得到了一个一般的证明搜索过程. Elf的高阶逻辑编程解释器使用深度优先搜索策略。这是不令人满意的，因为许多简单的规范根本无法执行。此外，由于冗余计算，性能可能不可接受。一个公平的搜索策略，如迭代深化，在元定理证明器BMF[17]中使用，使得左递归文法上的证明搜索可行，但正如实验所示，冗余计算也严重阻碍了性能。在本文中，我们讨论了基于备忘录的证明搜索的实验通过对子计算的记忆和重用，消除了部分冗余计算。这种记忆技术，也被称为制表，已经成功地应用于一阶逻辑编程，以解决复杂的问题，例如实现语法的识别器和解析器[20]，表示转换系统CCS和编写模型检查器[3]。XSB系统[16]证明了表格逻辑程序可以有效地执行，事实上可以与Prolog程序混合，以实现两全其美。在文献[15]中，我们给出了一个高层次的描述表高阶逻辑程序设计的基础上，演算和控制削减。在此基础上，我们已经实现了一个原型评估精灵程序。在本文中，我们使用两个应用程序比较了基于记忆化，深度优先搜索，迭代深化的证明搜索的性能1）使用子类型和交集类型的双向类型检查，以及2）解析成高阶抽象语法。实验表明，基于记忆化的证明搜索可以带来实质性的性能改进，使某些查询的执行完全可行。虽然我们在这里集中在LF的逻辑框架，这是Elf的基础，它似乎可以应用到λProlog [7]或Isabelle [9]，这是基于遗传Harrop公式和简单类型的条款。该文件的组织如下：在第二节。2.介绍了一种带子类型小型函数式语言，并提出了高阶表计算的思想。在高阶环境中面临的挑战在第二节中描述。3.节中4.讨论了该函数式语言的双向类型检查算法的实验，并将基于记忆化的证明搜索算法与传统的逻辑程序设计算法进行了性能节中5，我们讨论了将一阶公式解析为高阶抽象语法的实验，并将基于记忆化的证明搜索与基于迭代深化的证明搜索进行了比较。节中6.讨论相关工作，总结成果，并对今后的工作进行展望。皮恩特卡112关于我们2示例：子类型作为一个起点，我们介绍一个小型的函数式语言与子类型。我们还包括一个用于位串的示例数据类型位，以及用于自然数（没有前导零）的nat子类型，用于正数的pos子类型和0子类型。表达式e：：=ϵ |e0级|e1|林新益|第一季第二集|设u = e1在e2中|病例e，病例1|x 0 e2|x1件，3件类型τ：：=| 零|POS |Nat|位|τ1→ τ2我们将0和1表示为构造函数，并且将0表示为空字符串。例如，6表示为110。这个例子足够小，它允许我们说明基于LF设置中的记忆化的证明搜索的基本原理和挑战refl：sub T T.Zn：低于零的 自然状态 下：sub（T1=>T2）（S1=>S2）tr：subT Spn：sub posnat.<-subS1 T1<- subT Rnb：sub nat bit。<- sub T2 S2。<- subR S.tp_sub：ofE Ttp_lam：of（lam（[x]E x））（T1=> T2）<-E T<'- （ { x ： e x p }o fxT 1- >o f （ Ex ） T 2 ） } 。<- subT为了实现基于Horn子句集的子类型关系逻辑程序设计。然而，Elf比一阶逻辑编程丰富得多，并且还支持基于高阶抽象语法的优雅编码[14]。在构造函数中绑定的变量，如lam，将与Elf中的λ绑定。由λ-表达式λx.Ex描述的绑定使用Elf语法表示为[x] E x，而Mini-ML表达式lamx.e在Elf中表示为lam[x] E x。通过应用程序和β-归约来建模替代除了变量绑定构造，Elf支持从假设和处理参数进行推理。lam的类型规则的前提取决于新参数x和x是τ1类型的假设。而且我们假设如果需要，可以重命名e中的所有变量在Elf中，表示为（x：exp的x T1 ->的（E x）T2），其中 x：exp表示 普适的量化器：exp。我们可以证明（lam（[x] Ex））（T1 => T2），如果我们可以证明对于一个新的变量x，如果x的类型是T1，那么函数（E x）的函数体的类型是T2。更详细的讨论见[12]2。给定系统中的类型推理是高度不确定的。例如，一个逻辑编程解释器可能会陷入应用传递性规则导致无限循环的陷阱 此外，我们还反复进行了类型检查，表达式，出现不止一次。这可能会严重影响性能。2所有示例的代码可以在http://www.cs.cmu.edu/~bp/LFM02上找到皮恩特卡113阶段1零度以下AreflA =阶段2阶段3阶段4零反射trA =零A =nat低于零R，亚R AreflZnZnA =nat零度以下A亚天然AreflA =nattrsub natR，亚R ANBA =位(tr锌铌）A =位reflNBrefl A = Natsubnat AnbA=子位AreflA =位tr子比特R，refl子位A反射 A =位(tr锌铌）亚R A子位AreflA =位参赛答案参赛答案参赛答案参赛答案零度以下A A=零下零A A=零下零A A=零下零A A =零A =natA =natA=natA =位A =位A =位亚天然AA= natsub natAA= natsub natAA =natA =位A =位A =位子位AA=子位AA =位表格法通过维护子目标及其答案的表格，并根据表格中的答案解决子目标重复出现的问题来我们回顾了brie Tamaki和Sato为了演示表格计算，我们更详细地考虑了查询子零T的评估搜寻工作分多个阶段进行。该表有两个目的：1）我们记录搜索过程中遇到的所有子目标。如果当前目标不在表中，那么我们将其添加到表中并继续计算。如果当前目标是表条目的变体，则挂起节点处的计算。2)除了我们试图解决的子目标之外，我们还将计算结果存储在表中，作为子目标的答案列表为了简化本演示中的表格，我们没有在表格中显式地记录证书（证明项），尽管我们在实际实现中记录了一个证明框架如果需要的话，我们可以使用骨架来重建证明。这意味着我们不仅可以检测有限和冗余路径，还可以通过重用表中的答案来取得进展在每个阶段中，我们应用程序子句和表中的答案。图1说明了搜索过程。Fig. 1. 分段计算搜索树的根被标记为目标子零A。每个节点都标记有一个目标语句，每个子节点都是将程序子句或表中的答案应用于父节点最左边原子的结果 应用条款H←A1←A2. ←An导致子目标A1，A2，. ，其中所有这些子目标都需要满足。然后我们将扩展第一个子目标A1，携带其余子目标A2，.，Analong。如果一个分支被成功地解决了，我们显示得到的答案。为了区分程序子句解析和答案的重用，我们在树中有两种不同的边。 程序子句皮恩特卡114阶段1阶段2（lam [x] x）Ttp_sub of（lam [x] x）R，sub R Ttp_lamu：x T1x T2uT1 = P，T2 = P，T = P =>reflT = P => T(tp_lam [u] u）sub（P => P）Ttrsub（P => P）R，亚R TR1 P.子P R2tp_subu：x T1x R，sub R T2uu：x P sub P T2►►条目答案（lam [x] x）TT = P => Pu：x T1x T2T1 = P，T2= P条目答案（lam [x] x）TT = P => Pu：x T1x T2T1 = P，T2= Psub（P => P）TT = P => P亚R1 P.R1 = S，P = SR1 = 0，P = natR1 = pos，P =nat. . .图二. 恒等函数分辨率是实线，而通过重新使用来自表格的答案获得的边缘两者都使用用于派生子节点的子句名称进行标记。使用边缘处的标签，我们可以为给定的查询重建证明项。一般来说，我们将省略实际的替换，即父节点与程序子句统一，以避免混淆示例。为了确保我们为查询生成所有可能的答案，我们限制了对表中答案的重用。在每个阶段中，我们只允许重用在前一阶段生成的答案。前一阶段的答案（可用于答案解析）标记为灰色，而当前答案（尚不可用）标记为黑色。3LF的挑战在表格式高阶逻辑编程中，我们扩展了表格式来处理可能包含蕴涵和泛量化的子目标，我们的术语语言是依赖类型的λ-演算。表条目不再是原子目标，而是目标A和假设的上下文Γ。此外，项可能取决于对Γ的假设。为了突出一些挑战，我们讨论了对（lam[x]x）T的查询的评估（参见图2）。2）的情况。嵌套蕴涵和泛量化器的可能性为基于记忆的计算增加了新的复杂度。表上的检索操作需要重新设计。一个核心问题是如何查找目标Γa是否已经在表中。有两个选项：第一个选项中，我们只检索给定上下文Γ的目标a的答案，如果目标和上下文一起匹配表中的条目ΓJaJ。 在第二个选项中，我们将子目标a与表的目标aJ项ΓJaJ，并将ΓJ中的假设视为额外的子目标，从而延迟满足这些假设。 我们选择第一种方法皮恩特卡115目标连同其动态上下文ΓJ。一个原因是它限制了搜索早期可能检索的数量，以及满足这些动态假设的可能例如，为了求解子目标u：ofx T1<$ofx R，subR T2，我们专注于求解最左边的目标u：ofx T1<$ofx R记住我们仍然需要求解u：ofx T1<$subR T2. 由于存在xT1=xT2的表项u：，其是当前目标u：xT1=xR的变体，因此计算被暂停。由于高阶设置，谓词和项可能依赖于Γ。Virga [19]在他的博士论文中开发了一种称为从属检查的技术，用于在执行前静态分析Elf使用基于从属关系的类型依赖分析[19]，我们可以检测和消除这种依赖。这允许我们在搜索树中检测更多的循环，即更多的节点可以被挂起，因为它的变体已经在表中。另一优化涉及在上下文T中对假设的处理。当将目标A与上下文Γ存储在一起时，并非动态上下文Γ中的所有假设都可能有助于目标G的证明。 例如，在评估上面的查询我们得到以下两个子目标：ofx T1subR T2和subR T2。任何解决方案的目标子R T2将是独立的假设x T1。我们可以再次使用基于从属关系，以加强上下文，从而导致更小的表和消除更多的冗余和无限的路径。虽然使用记忆化的计算对于具有传递闭包或左递归的程序产生更好的性能，但Prolog风格的计算对于右递归更有效例如，Prolog对于简单的右递归文法具有线性复杂度，但对于memoization，评估可能是二次的，因为调用需要使用显式复制记录在表中。因此，重要的是要允许表谓词和非表谓词自由混合，并能够选择对当前情况最有效的策略因此，在当前的原型中，如果用户希望使用memoization，则声明谓词为table. Mixing tabled. Non-table.Predicates是必不可少的，以获得有效的证明搜索引擎。4示例：细化类型检查在本节中，我们讨论了Davies和Pfenning [4]开发的具有交集类型的小型函数语言的双向类型检查算法的实验。在具有子类型和交集类型的函数语言中，类型推断通常被认为是不切实际的，因为不存在主类型。双向类型检查背后的思想是区分可以合成类型的表达式和可以针对给定类型进行检查的表达式。程序员指定一些类型来指导为某些表达式推断类型。皮恩特卡116∧ → → ∧ → → ∧ →→→→可推断I：：=x|ϵ|I0|I1|应用IC|C：τ可检查项C：：=I|Lamx.C|设u = IinC|第一个病例为C1型肝炎|x 0 °C2|x1C3其意图是，给定上下文Γ和表达式I，我们使用类型推断来表明表达式I具有类型τ，并使用类型检查来验证表达式C具有类型τ。在双向类型检查算法的实现中，可以有许多方式来导出I具有类型τ，并且类似地，有多于一种方式来检查C具有给定类型τ。讨论完整的双向类型检查算法超出了本文的范围，感兴趣的读者可以参考Davies和Pfenning的原始论文[4]。我们使用的双向类型检查器在精灵Pfenning的实现。类型检查器可以用原始的逻辑编程解释器执行，它执行深度优先搜索。然而，冗余计算可能会严重阻碍其性能，因为有几个推导证明程序具有特定类型。例如，有20，000种方法可以显示程序plus具有交集类型（nat nat）（nat pos pos）（pos nat pos）（pos pos pos）。可能有人会说，我们只对证明加号具有特定类型的一个证明感兴趣，而不是对所有证明感兴趣。然而，它表明已经相当小的程序涉及大量的冗余计算。比快速成功更重要的可能是快速失败，如果加号没有指定的类型。快速失败在调试程序中是必不可少的，几分钟的响应时间是不可接受的。在实验中，我们测量探索整个证明树所需的时间这给了我们一个指示，在搜索空间中有多少冗余。当检查一个项C与一个类型τ时，我们使用memoization。基于记忆化的证明搜索采用了强化和变式检查。我们已经测试了加法、减法和乘法的程序请注意，例如，为了对乘法程序进行类型检查，我们还需要对所使用的任何辅助程序（如加法和移位）进行类型检查。与每个程序名称相关联的数字表示与其相关联的交叉点类型的深度例如，plus4意味着我们通过使用交集为plus分配了4个类型。mult1a表示我们将一种可能的类型与乘法程序相关联。如果一个程序标签被标记为（np），这意味着这个查询没有解决方案，类型检查器应该拒绝这个查询。对于类型检查程序，基于记忆化的加法和乘法证明搜索这是令人惊讶的，因为目前没有复杂的索引用于访问表。这表明，已经简单的记忆机制可以大大提高性能。在乘法的情况下，它使类型检查成为可能。我们在10小时后停止了深度优先搜索程序当然是证据搜索皮恩特卡117程序深度优先Memoization联系我们#SuspGoals+ 4483.070秒2.330秒15148加4696.730秒3.150秒17174加4（NP）22.770秒1.95秒14356sub'1a0.070秒0.240秒5811sub'3a0.130秒0.490秒9220sub1a3.52秒7.430秒251135sub1b3.88秒7.560秒252138亚3a10.950秒9.970秒277167sub3b10.440秒11.200秒278170mult1（np）1133.490秒4.690秒21783mult1a807.730秒4.730秒21178mult1b2315.690秒6.050秒226101mult1c2963.370秒5.310秒226107mult4∞17.900秒298270mult4（np）∞13.140秒275194表1查找所有解决方案：深度优先与基于记忆的搜索在存储和访问表中的目标时有一些开销。 如减法程序所示，这种开销可能会降低基于记忆的证明搜索的性能。 当类型检查减法程序时，深度优先搜索在前5个示例程序中的性能优于基于记忆的搜索。然而，在最后一个例子中，基于记忆的搜索胜过了深度优先搜索。为了公平起见，我们还包括两种搜索策略之间的比较，当我们在找到第一个答案后停止很明显，目前找到一个可解决的类型检查问题的第一个解决方案（即它是可证明的，程序具有指定的类型）总是需要更长的证明搜索基于记忆这表明在当前的实现中访问表仍然是相当昂贵这并不奇怪，因为到目前为止还没有实现索引。基于记忆的搜索做得相当差的另一个原因是由于多阶段搜索策略。尽管此策略相对容易实现和理解，但它将对表中存在的答案的检索限制为生成的答案皮恩特卡118程序深度优先Memoization联系我们#SuspGoals+ 40.08秒0.180秒540加40.1秒0.430秒720加4（NP）22.770秒1.95秒14356sub'1a0.050秒0.240秒6411sub'3a0.110秒0.410秒9220sub1a0.250秒6.210秒251135sub1b0.250秒5.020秒242121亚3a0.280秒7.80秒277161sub3b0.350秒8.160秒278164mult1（np）1133.490秒4.690秒21783mult1a0.160秒2.900秒20160mult1b0.180秒4.090秒22290mult1c0.170秒2.930秒21160mult40.250秒7.150秒272181mult4（np）∞13.020秒275194表2寻找第一个解决方案：深度优先与基于记忆的搜索在前几个阶段。这会导致子目标被挂起，尽管答案可能是可用的，并且延迟了对这些子目标的求解。出于这个原因，XSB使用SCC（强连接组件）调度策略，该策略允许在表中的答案可用时立即重用但是，当比较类型检查器拒绝程序所需的时间时，基于记忆的搜索的好处是显而易见的，如示例plus4（np）和mult1（np）所示。总体而言，基于记忆化的搜索的性能更加一致，即，接受或拒绝一个节目大约需要相同的时间为了使双向类型检查在实践中合理有效，Davies和Pfenning目前研究了一种算法，该算法综合了可推断项的所有类型，并通过使用布尔约束来跟踪适用的类型然而，这远非微不足道，通过添加对记忆化的显式支持来细化Elf实现，使类型检查器复杂化因此，作为执行的结果而产生的证书更大，并且包含对显式记忆数据结构的引用这在认证代码的上下文中尤其不可取，皮恩特卡119¬⇒传输给消费者并由消费者检查，因为发送较大的证书占用更多的带宽，检查它们需要更多的时间。此外，证明具有特殊记忆支持的类型检查器的正确性将是困难的，因为我们需要明确地推理记忆的结构。实验结果表明，基于记忆化的证明搜索有可能将双向类型检查算法转化为一个高效的类型检查器，而不需要为用户进行额外的排序5示例：公式语法的识别算法和解析器是说明表格求值的好处Warren [20]指出，在Prolog中实现上下文无关语法会导致递归下降识别器，而表逻辑编程将相同的语法转换为Early算法的变体此外，表格逻辑编程允许我们执行左和右递归语法，否则将在Prolog风格的执行下循环（例如，左递归的）。我们说明表计算与解析一阶公式到高阶抽象语法。一阶公式的定义与通常一样。命题一：：=原子P|欧元|A&A|A对A|A→A|真正|虚假|对于所有x.A|存在x.A|（一）术语可以是常量、变量或带参数的函数 原子命题要么是命题常量，要么是以项为自变量的谓词。 除了给定的语法之外，我们还强加了以下优先顺序：> &>v>.合取和析取是左结合的，蕴涵是右结合的。fall：fqC<-（{x：id} fq（（bvar I x）# C）F F '（P x））。fex：fqC<- （{x：id} fq（（bvarIx）# C）F F '（Px））。 cq：fq C F F'<-fiCFF%隐含--右结合fimp： fiCFF<- foC F<-fi C F1 F ' P 2 .ci：fiCF F<- foCFF%分离-左结合：fo C F F<- foC F<-fa C F1 F ' P2.解析器获取绑定变量的上下文、两个标记列表和皮恩特卡120返回以高阶抽象语法表示的有效公式[14]。最初，绑定变量的上下文是空的，第一个令牌列表表示输入流，第二个列表是空的，P最终将包含结果。使用高阶抽象语法，在构造函数中绑定的变量，如forall和exists，将与Elf中的λ绑定。实现蕴涵、合取和析取的左和右结合性属性的最简单方法是混合使用右和左递归程序子句。合取和析取的子句是左递归的，而蕴涵的程序子句是右递归的。这种语法的实现是直接的，反映了定义的属性，如左和右结合性和优先顺序。然而，当使用传统的逻辑编程解释器执行时，语法的执行将无限循环。因此，我们比较了一些示例程序的执行，这些程序使用基于记忆化的证明搜索和基于迭代深化的证明搜索，如当前的定理证明器BMF[17]所执行的。迭代深化搜索要求用户提供深度范围。值得指出的是，迭代深化搜索将在找到第一个解或达到深度界限后停止，而基于记忆的搜索将在找到解（并表明不存在其他解）或证明不存在其他解这意味着，我们不能使用迭代深化搜索来决定是否应该接受给定的令牌流，而基于记忆的搜索会产生一个决策过程。输入长度Iter。深化Memoization联系我们#SuspGoals50.020秒0.010秒1511201.610秒0.260秒605432208.010秒2.020秒17619756∞7.980秒371439107∞86.320秒9291185表3基于迭代深化和记忆化搜索实验表明，基于记忆化的证明搜索为判定给定的标记流是否属于公式语言提供了一种更为有效的方法事实上，对于长度大于50个token的输入流，我们在几个小时后停止了迭代深化过程注释1：值得注意的是，一般来说，向输入语法的非终结符添加额外参数（表示每个规则生成的解析树部分）并自然地添加构造解析树的必要代码的直接皮恩特卡121→ ∧ →→从复杂性的角度来看是非常不令人满意的多项式识别算法可以转化为指数算法，因为对于给定的输入字符串，可能存在指数级多个解析树。然而在这个例子中，每个公式都只有一个解析跟踪，因此向识别器添加一个额外的参数只会增加一个常量因子。注2：我们可以将输入字符串作为一组事实存储在数据库中，而不是将其表示为我们可以认为输入流中的每个标记都从1开始编号。然后我们将字符串存储为一组形式为单词1 'forall'的事实。单词2“x”。等等，其中单词itok i表示输入流的第i个令牌。6相关工作和结论已经提出了许多类似于Elf的不同框架，例如λProlog [7，5]或Isabelle [9，10]。Elf基于LF型理论，λProlog和Isabelle基于遗传Harrop公式。在这些框架中支持定理证明的传统方法是使用策略和战术来指导证明搜索。策略将带有一些未证明叶子的证明结构转换为另一个证明结构。Tactical将策略结合起来，以执行证明中更复杂的步骤。战术和战术是用ML或其他一些战略语言编写的。为了有效地推理某些特定信息，用户实施特定的策略来引导搜索。这意味着战术必须根据不同的具体情况重新编写。此外，用户必须了解如何指导证明者找到证明，这通常需要有关系统的专业知识证明策略的正确性本身就是一个复杂的定理证明问题。Elf采用的方法是赋予框架逻辑编程的操作语义，并为其设计通用的证明搜索策略。用户可以专注于开发高级规范，而不是让证明搜索工作。实现的正确性仅通过类型检查来强制初步实验表明，基于记忆的证明搜索是一个功能强大的搜索引擎。基于记忆化的证明搜索只能为给定查询找到一个代表性证明，因此它本质上 是 不 完 整 的 。 例 如 ， 当 类 型 检 查 加 上 （ nat→nat→nat ） 时 ，（nat→pos→pos）（pos→nat pos）（pos pos pos）在传统的逻辑编程解释下有许多证明，但我们将只找到一个基于记忆的搜索。然而，我们往往不想和需要区分不同的证明公式A，但只关心存在的证明A连同一个证明项。在[13]中，Pfenning为证明不相关性开发了一个依赖类型理论，并讨论了逻辑框架中的潜在应用这使得我们可以把所有的证明A作为平等的两个证明被认为是在未来，我们计划将基于记忆化的证据搜索结合起来皮恩特卡122和证明无关性的方法从原型收集的经验来看，似乎其他逻辑编程语言（如λProlog）也会从基于记忆的搜索中获益。虽然我们在设计原型时已经注意到了这一点，但仍有很大的改进余地当前最紧迫的问题是实现表的索引以实现快速表访问。致谢：作者感谢与Frank Pfenning和David S.Warren就这项工作进行的多次讨论。也感谢你的帮助，来自卡斯滕·斯库尔曼、博·哈普和凯文·沃特金斯。这项工作得到了NSF Grant CCR-9988281的部分支持。引用[1] Andrew W.作者声明：Amy P.一种用于证明携带代码的类型和机器指令的语义模型。在第27届ACM SIGPLAN-SIGACT Symposium on Principles ofProgramming Languages（POPL '00），第243- 253页，2009年1月。两千[2] W. Chen和D. S.沃伦一般逻辑程序的延迟表式求值。Journal of the ACM，43（1）：20-74，January 1996.[3] B. Cui，Y.Dong，X.Du，K.N. Kumar，C.R.Ramakrishnan，I.V.拉马克里什南，A. Roychoudhury ， S.A. Smolka 和 D.S. 沃 伦 逻 辑 编 程 和 模 型 检 查 。 在Principles of Declarative Programming（Proceedings of PLILP/ALPSpringer-Verlag，1998.[4] 罗恩·戴维斯和弗兰克·普芬宁相交类型和计算效应。 在Proceedings of theInternational Conference on Functional Programming （ ICFP 2000 ） ，Montreal，Canada，pages 198-208.北京：人民出版社，2000年。[5] 艾米·费登。在高阶逻辑编程语言中实现战术和战术。Journal of AutomatedReasoning，11（1）：43-81，August 1993.[6] 罗伯特·哈珀，浮里奥·洪塞尔，戈登·普洛特金。定义逻辑的框架。Journalof the Association for Computing Machinery，40（1）：143[7] Gopalan 纳达图尔 和 戴尔 米勒 一个 概述 的 λProlog。第五届国际逻辑编程会议，第810-827页，西雅图，华盛顿，1988年8月。麻省理工学院出版社.[8] G. Necula和S. Rahul.基于Oracle的不可信软件检查。第28届ACM程序设计语言原理研讨会（POPL01），2001年。[9] 劳 伦 斯 角 ， 澳 - 地 保 尔 森 自 然 演 绎 作 为 高 阶 分 辨 率 。 Journal of LogicProgramming，3：237皮恩特卡123[10] 劳伦斯角，澳-地保尔森伊莎贝尔：接下来的700个定理证明者。第九届自动演绎国际会议论文集，第772-773页，Argonne，Illinois，1988。第310章大结局系统抽象。[11] 弗兰克·芬宁Elf：一种逻辑定义和验证Meta编程的语言。在第四届计算机科学逻辑年度研讨会上，第313-322页，加利福尼亚州太平洋格罗夫，1989年6月。IEEE计算机学会出版社.[12] 弗兰克·芬宁计算和演绎。 剑桥大学出版社，2000年。准备中。1997年4月起的草稿有电子版。[13] 弗兰克·芬宁模态类型理论中的内涵性、外延性与证明无关性第16届IEEE计算机科学逻辑年会，波士顿，美国，2001年。[14] 弗兰克·普芬宁和科纳尔·埃利奥特高阶抽象语法。ACM SIGPLAN '88语言设计与实现研讨会论文集，第199-208页，佐治亚州亚特兰大，1988年6月[15] 布里吉特·皮恩特卡。 证明理论基础 为 提交 高阶逻辑程序在第18届逻辑编程国际会议上，丹麦哥本哈根，LNCS，页面出现。Springer-Verlag，2002.[16] 康斯坦丁诺斯·萨戈纳斯和特伦斯·斯威夫特一种抽象机，用于执行固定顺序的分层逻辑程序。ACM Transactions on Programming Languages and Systems，20（3）：586[17] CarstennSchürma nnanddFr annkPf enn in g.在LF的一个简单元逻辑中实现了该算法。第15届自动演绎国际会议（CADE-15），第286-300页，德国林道，1998年7月。第1421章.[18] H. Tamaki和T.佐藤 旧决议与制表。 在Proceedings of the 3rd InternationalConference on Logic Programming，Volume 225 ofLecture Notes in ComputerScience，pages 84Springer，1986年。[19] 罗伯托·维尔加使用依赖类型的高阶重写。卡内基梅隆大学数学科学系博士论文，2000年。[20] David S. 沃 伦 表 式 逻 辑 程 序 设 计 中 的 程 序 设 计 。草 稿 可 查 阅 http ：//www.cs.sunysb.edu/tagwarren/xsbbook/book.html，1999年。