集成SAT求解器和LCF式定理证明器的方法和应用

理论计算机科学电子笔记144（2006）67-78www.elsevier.com/locate/entcs将SAT求解器与LCF类型的定理证明器Tjark Weber杰克·韦伯1，2在这一点上，TechnischeUiversi tta t tMunchenBoltzmannstr. 3，D-85748Garchingb. München，Germany摘要本文介绍了一个领先的SAT求解器与Isabelle/HOL，一个流行的互动定理证明器的集成。SAT求解器为命题重言式（的实例）生成解析式证明。这些证明是由定理证明者验证的。所提出的方法显着提高了Isabelle保留字：SAT求解器，命题求解，证明检查，LCF式定理证明器1引言像PVS [22]，HOL [13]或Isabelle [23]这样的交互式定理证明器传统上支持丰富的规范逻辑。然而，这些逻辑的证明搜索和自动化是困难的，并且证明非平凡定理通常需要专家用户的手动指导另一方面，自动定理证明器虽然通常是为更简单的逻辑设计的，但在过去几年中变得越来越强大新的算法、改进的算法和更快的硬件使得有趣的定理可以在很少或根本没有人类交互的情况下被证明，有时甚至在几秒钟内。1这项工作得到了德国研究基金会计算机科学逻辑博士项目的支持2 电子邮件地址：webertj@in.tum.de1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.12.00768T. Weber/Electronic Notes in Theoretical Computer Science 144（2006）67通过将自动化证明器与交互式系统相集成，我们可以保留我们规范逻辑的丰富性，同时提高自动化程度[25]。这是一个至少可以追溯到90年代初的想法[17]。然而，为了确保自动证明器中的潜在错误不会使整个系统变得不可靠，Isabelle中的定理，就像其他LCF风格的证明器一样，只能通过一组核心推理规则来推导因此，自动证明器返回公式是否可证明是不够的，但它还必须生成实际的证明，根据交互式系统的推理规则表达（或可表达）形式验证是交互式定理证明的一个重要应用领域。验证中的问题通常可以简化为布尔满足性（SAT），最近SAT求解器的进步使这种方法在实践中可行。因此，交互式证明器在命题问题上的表现可能具有重要的实际意义。在本文中，我们描述了zCha [20]（一种领先的SAT求解器）与Isabelle/HOL [21]证明器的集成我们发现，使用zCha证明定理的命题逻辑显着提高了伊莎贝尔然而，尽管伊莎贝尔先前的决策程序在未经证实的情况下失败了，能够证明，zCha能够产生具体的反例。下一节将更详细地描述zChaeMap与Isabelle/HOL的集成在第3节中，我们评估我们的方法的性能，并报告实验结果。相关工作在第4节中讨论。第五节对本文进行了总结，并指出了今后的研究方向。2系统描述为了证明Isabelle/HOL系统中的一个命题重言式φ，我们使用zCha证明，我们分几步进行首先对φ取反，并将其转化为合取范式的等价公式φ然后，φ被写入DIMACS CNF格式的文件[7]，zCha（和许多其他SAT求解器）支持的输入格式。zCha在这个文件上运行时，返回在后一种情况下，向用户显示令人满意的分配。这个赋值构成了原猜想的一个反例。然而，当zCha返回“unsatisfiable”时，事情就变得更加复杂了。如果我们对SAT求解器有信心，我们可以简单地相信它的结果，并接受φ作为Isabelle中的定理。该定理被标记为在这种情况下，zCha中的一个错误可能允许我们导出T. Weber/Electronic Notes in Theoretical Computer Science 144（2006）6769伊莎贝尔zChaffDIMACS CNF输入公式预处理满意？是否分配反例微量定理证明重建Fig. 1. 系统架构Isabelle/HOL中的不一致定理相反，LCF方法要求我们在Isabelle/HOL中验证zCha虽然这并不像验证一个令人满意的分配那么简单，但SAT求解器的日益复杂性已经提出了支持独立验证其结果的问题，并且在2003年，L.Zhang和S.Malik [30]生成可以由独立检查器验证的分辨率风格的证明（这就是为什么我们选择zCha作为SAT求解器与Isabelle集成的原因。用证明生成能力扩展其他基于DPLL的求解器应该相对简单[30]，但尽管在这个方向上做了一些工作[10]，据我们所知，zCha是目前唯一公开可用的证明生成SAT求解器。因此，我们的主要任务归结为使用Isabelle/HOL作为zCha证明发现的解决方案的独立检查器zCha将此证明存储在Isabelle读取的文本文件中，并在Isabelle/HOL中重播各个解决步骤。第2.1节描述了输入公式的必要预处理，证明重构的细节在第2.2节中解释。整个系统架构如图1所示。2.1预处理Isabelle/HOL o语言支持高阶逻辑（在Isabelle的Meta逻辑之上因此，（求反的）输入公式φ必须在传递给zCha φ之前进行预处理。70T. Weber/Electronic Notes in Theoretical Computer Science 144（2006）67Meta逻辑的第一类连接词元蕴涵和元等价被相应的HOL连接词所−→和=。这只是一个技术问题。然后从φ中删除布尔常量True和False，以及蕴涵、−→和等价，=.唯一剩下的连接词是连接词、分离词和否定词。最后将φ转化为否定范式，再转化为合取范式（CNF）.目前实现了两种不同的CNF转换：一种可能导致公式指数爆炸的朴素编码，以及一种可能引入（存在量化的）辅助布尔变量的Tseitin风格编码[28]。[12 ]第10段。φ的量子化子公式被视为原子。注意，在CNF中将φ转换成等价公式φJ相反，我们必须在Isabelle/HOL中证明这种等价性。结果不是一个单一的公式，而是一个形式为φ=φJ的定理。我们构造这个定理的主要工具是由A.Chaieb和T.Nipkow [6]：t=let的分解(ts，recomb）=分解tin recomb（map（thm_of decomp）ts）它取一个类型为α→αlist×（βlist→β）的分解函数decomp和一个类型为α的问题t，将t分解为一系列子问题ts和一个重组函数recomb，递归地求解子问题，并使用recomb将递归解组合成一个整体解。在我们的设置中，t是一个公式，decomp将查看它的句法结构（即它最外面的连接词），β是定理的类型 当t只是一个字面量时，我们使用=的反射性来导出t = t。重言式如<$P=PJ=<$$>Q=QJ=<$$>（P<$Q）=PJ<$QJ（在Isabelle/HOL中很容易证明）被用来实现重组函数。例如，这个对应于德摩根定律之一，并且是到否定范式的转换的一部分。上面提到的所有转换都可以通过适当的分解实例化来处理。zCha将子句视为文字的集合，隐式地使用关联的析取的唯一性、交换性和恒等式。因此，除了转换为CNF之外，还需要利用合取和析取的结合性，我们将φJ改写为一个等价的CNF公式，去掉了不必要的括号。在第二步中，我们删除重复的文字，使每个子句包含每个文字最多一次。最后，使用PP= True，我们删除了每个包含文字及其否定的子句。每个预处理步骤产生一个等价定理，T. Weber/Electronic Notes in Theoretical Computer Science 144（2006）6771在Isabelle/HOL中得到了证明，并且=的传递性允许我们将这些定理组合成一个定理φ=φ，其中φ是我们转换的最终结果。除非φ在语法上已经等于True或False，否则它将被写入DIMACS CNF格式的文件，并在此文件上调用zCha。2.2证明重建当zCha返回这个文件由三个部分组成：通过解决方案从原始问题导出的子句，这些子句隐含的变量值，以及一个连接子句，即。所有文字都为假的派生子句文本文件由Isabelle解析，其中包含的相关信息用于重建不满意度Isabelle/HOL中的证明证明重构基于两个简单的函数：一个函数证明子句，它使用分解从现有定理φ−→c1，.导出形式为φ−→c的 φn−→cn（其中c和C1，…，cn是单个子句），另一个函数proveliteral从l的先行项φ−→ c证明φ−→l（其中l是单个文字）这里c必须是包含l的子句，并且对于c中的所有其他文字lJ，形式为φ−→ <$lJ的定理必须是可证明的。这些函数分别对应于zCha编译器生成的文本文件的第一部分和第二部分。证明条款clause_id =resolution（map prove_clause（resolvents_of clause_id））prove_literal var_id=letth_ante = prove_clause（antecedent_of var_id）var_ids =filter（fni =>i> var_id）(var_id_in_clause th_ante）在解析中（th_ante：：map prove_literal var_ids）resolvents of和antecedent of是辅助函数，它们依赖于zCha语法提供的信 息 来 分 别 返 回 子 句 的 resolvents 或 变 量 的 antecedent 的 IDvar ids inclause，当应用于形式为φ−→c的定理时，返回出现在子句c中的变量的ID。两个子句c1和c2之间的解析总是用c1中的第一个字面值来执行，而这个字面值在c2中出现相反的极性。注意，解析必须在内部使用结合性和交换性的析取来重新排序子句，并使用等元性来确保结果子句最多包含一次每个文字。72T. Weber/Electronic Notes in Theoretical Computer Science 144（2006）67证据重建分三步进行。首先，通过调用prove子句来证明冲突子句。然后，对冲突子句中的每个文字都调用proveliteral，以表明该文字必须为假。最后，用这些否定的字面量解决冲突子句，得到定理φ−→False。出于效率的原因，实际的实现与上面显示的略有不同一些由zCha证明导出的子句可能在证明过程中被多次使用，而另一些则可能根本不使用。因此，被证明过一次的定理被存储在两个数组中（一个用于子句，一个用于文字），如果再次需要它们，它们只需要查找因此，我们的实现不是纯功能性的。2.3一个简单的例子在本节中，我们使用一个小例子来说明证明重构考虑以下输入公式φ（<$v 1 <$v 2）<$（<$v 2 <$$>v 3）<$（v 1 <$v 2）<$（<$v 2<$v 3）。由于φ已经是合取范式，预处理简单地产生定理φ=φ。相应的DIMACS CNF文件，除了它的头，包含一行用于φ中的每个子句：-12 0-2 -3 012 0-23 0zCha可以轻松地检测到这个问题是不可满足的，并创建一个包含以下数据的文本文件：CL：4=20VAR：2L：0V：1A：4Lits：4VAR：3L：1V：0A：1Lits：57形态：3 == 5 6这告诉Isabelle，首先，一个新的子句（ID为4）是通过用子句0，<$v1<$v2解析子句2，v 1<$v 2得到的在子句2和子句0中出现的第一个正和负变量是v1;这个变量是通过决议消除。现在变量2的值（VAR：2）可以从子句4（A：4）推导出来。v2必须为真（V：1）。子句4只包含一个文字（Lits：4），即v2（因为4mod 2 =2），正发生（因为4 mod 2 = 0）。该决策在级别0（L：0）做出，在更高级别的任何决策之前。T. Weber/Electronic Notes in Theoretical Computer Science 144（2006）6773同样，变量3的值可以从子句1推导出，3. v3必须为false（V：0）。最后，第3条是我们的合同条款。它包含两个文字，<$v 2（因为5 <$2= 2，5 mod 2 = 1）和v 3（因为6 <$2 = 3，6 mod 2 = 0）。但是我们已经知道两个字面值都必须为假，所以这个子句是不满足的。请注意，关于决策级别、变量的实际值或子句中出现的文字的信息是多余的，因为Isabelle不需要这些信息来验证zCha的这些信息总是可以从原始问题中重建出来。还要注意，Isabelle中的实际证明重构是从冲突条款开始向后进行的。这样做的优点是，zCha记录的但不需要显示不满意的分辨率步骤不会在Isabelle中重放。在我们的例子中，第一个条款3被证明（是微不足道的，因为它是原始子句之一）。然后调用proveliteral 2，立即导致调用prove子句 4。 子句4是通过用子句0分解子句2来证明的。现在调用了proveliteral 3，由于子句1，变量3的先行词，也包含变量2，这导致了另一个proveliteral 2的调用。最后，矛盾可以通过解决冲突子句，子句3，与证明文字2和证明文字3的结果来推导。3评价Isabelle/HOL证明器有三个主要的自动证明程序：auto，它执行目标的简化和分裂，blast[24]，一个基于表格的证明器，以及fast，它使用标准的Isabelle推理搜索证明详情见[21]。我们将我们的方法与Isabelle现有的证明程序在TPTP库[ 27 ]的2.6.0版中包含的所有42个问题上的性能进行了比较，这些问题在命题中表示。逻辑这些问题被否定了，因此无法满足的问题变得可以证明。所有的基准测试都是在一台拥有3 GHz Intel Xeon CPU和1 GB主内存的机器上运行的。这42个问题中有19个相当简单，并且通过现有程序和SAT求解器方法在不到一秒的时间内解决了每个问题。表1显示了解决其余23个问题所需的时间（以秒为单位）x表示过程内存不足或未能在一小时内终止。Isabelle/HOL中的证明重建目前比使用C++编写的外部检查器[30]进行证明验证慢几个数量级虽然ISA中仍有很大的优化潜力，74T. Weber/Electronic Notes in Theoretical Computer Science 144（2006）67问题地位汽车爆炸快速zChaMSC007-1.008不饱和。XXX726.5NUM285-1饱和XXX0.2PUZ013-1不饱和。0.5X5.00.1PUZ014-1不饱和。1.4X6.10.1PUZ015-2.006不饱和。XXX10.5PUZ016-2.004饱和XXX0.3PUZ016-2.005不饱和。XXX1.6PUZ030-2不饱和。XXX0.7PUZ033-1不饱和。0.26.40.10.1SYN001-1.005不饱和。XXX0.4SYN003-1.006不饱和。0.9X1.60.1SYN004-1.007不饱和。0.3822.22.80.1SYN010-1.005.005不饱和。XXX0.4SYN086-1.003饱和XXX0.1SYN087-1.003饱和XXX0.1SYN090-1.008不饱和。13.8XX0.5SYN091-1.003饱和XXX0.1SYN092-1.003饱和XXX0.1SYN093-1.002不饱和。1290.816.21126.60.1SYN094-1.005不饱和。XXX0.8SYN097-1.002不饱和。X19.2X0.2SYN098-1.002不饱和。XXX0.4SYN302-1.003饱和XXX0.4表1TPTP问题belle/HOL实现（参见第4节），分析表明，这种差异也必须归因于IsabelleT. Weber/Electronic Notes in Theoretical Computer Science 144（2006）6775的LCF风格内核提供的数据结构和函数SAT求解器方法大大优于以前在Isabelle/HOL中可用其他程序结合起来只解决了8个较难的问题。不同程序之间的运行时间相比之下，SAT求解器方法可以解决所有问题，除了两个问题之外，其他问题都需要不到两秒钟的时间，并且为无法证明的问题提供了实际的反例此外，表1的最右边的列已经示出了用于调用zCha的总（组合）时间以及以下在Isa中的证明重构76T. Weber/Electronic Notes in Theoretical Computer Science 144（2006）67belle/HOL. zCha在通常可以忽略不计的一小部分时间后终止，此时已经可以向用户显示一个确定的答案4相关工作Michael Gordon实现了HolSatLib[12]，这是一个现在是HOL 4定理证明器的一部分的库该库提供了将HOL 4项转换为CNF的函数，并使用SAT求解器对其进行分析。然而，在不满意的情况下，用户只能选择信任外部求解器。没有证明重建发生，SAT求解器中的一个错误可能最终导致HOL 4中的不一致也许与我们的工作更密切相关的是自动化一阶证明器的集成，最近JoeHurd [15，16]和Jia Meng [18，19]进一步探索了这一点。自动化系统找到的证明要么由交互式证明器立即验证[15]，要么转换为可以稍后执行的证明脚本[19]。然而，他们工作的主要重点是从交互式证明器的规范语言到一阶逻辑的必要翻译相反，我们的方法到目前为止仅限于命题重言式的实例，但它避免了困难的翻译问题，并使用SAT求解器，而不是一阶证明器。Clark Barrett等人[5]将定制的SAT求解器与CVC Lite系统[4]集成。虽然这个求解器产生的证明可以独立检查，但我们的工作表明，将现有的高效求解器与LCF风格的证明器集成是可能的：最新版本的zCha证明器提供的信息足以在定理证明器中产生证明对象，不需要定制的求解器。最近，我们的工作被Alwen Tiu等人所采用。[9]，他们通过广泛使用Isabelle的Meta逻辑和转换子句l 1...... ln等于<$l1=. =ln= False.这避免了明确使用结合性以及在每个归结步骤中析取到重排子句的交换性我们已经实现了基于这些想法的证明重建的优化版本 该实现现在是Isabelle2005发行版的一部分，能够在8秒内解决表1中的所有问题（包括问题MSC 007-1.008）。此外，Hasan Amjad [1]最近以类似的方式将MiniSAT求解器[8]的证明生成版本与HOL 4集成在一起。SAT求解器在定理证明中的其他应用-T. Weber/Electronic Notes in Theoretical Computer Science 144（2006）6777包括基于SAT的决策过程（例如[3，26]），以及基于SAT的模型生成技术（例如[2，29]）。这些应用程序再次需要涉及的翻译，正确实现SAT求解器通常是理所当然的。5结论和今后的工作我们的研究结果表明，zCha的基于策略是明显优于Isabelle在zCha的帮助下，许多以前不在Isabelle内置策略范围内的公式现在可以自动证明-或反驳-通常在几秒钟内。伊萨-贝尔然而，Isabelle他们的庞大规模目前不允许一个有效的治疗内伊萨-贝尔/HOL。进一步的工作是必要的，以调查这个问题是否可以通过对Isabelle的内核进行相对较小的优化来本文提出的方法具有超越命题推理的应用。更丰富逻辑（片段）的决策问题可以简化为SAT [3，26]。因此，命题逻辑的证明重构可以作为其他逻辑的证明重构的基础基于我们的工作，人们只需要一个证明生成实现的reduc-tion集成整个SAT为基础的决策过程与LCF风格的定理证明。确认作者要感谢Sharad Malik和Zhaohui Fu对zCha的帮助，以及Tobias Nipkow和匿名裁判的宝贵建议。引用[1] 哈桑·阿姆贾德 HOL/Minisat接口。 个人通信，2005年10月。[2] Pranav Ashar，Malay Ganai，Aarti Gupta，Franjo Ivancic，and Zijiang Yang. 有效的基于SAT的有界模型检验软件验证。2004年，第78T. Weber/Electronic Notes in Theoretical Computer Science 144（2006）67[3] G. Audemard，P. Bertoli，A. Cimatti，A. Kornilowicz和R. 阿提亚尼 一个基于SAT的解决布尔和线性数学命题公式的方法。 在Andrei Voronkov，编辑，Proceedings of the 18th InternationalConference on Automated Deduction（CADE-18），Volume 2392 ofLecture Notes in ArtiFicial Intelligence，pages 195 斯普林格。[4] 克拉克·巴雷特和谢尔盖·贝雷辛。CVC Lite：协作有效性检查器的新实现。第16届计算机辅助验证国际会议，美国马萨诸塞州波士顿，2004年7月。[5] Clark Barrett、Sergey Berezin和David L. 迪尔 一个生成证明的布尔搜索引擎。在自动推理中决策程序的语用学研讨会（PDPAR 2003），迈阿密，佛罗里达州，美国，2003年7月。[6] 阿明·柴伯和托拜厄斯·尼普科Presburger算法的一般证明合成。Tec hn icalreport，Tech n ischeUniverrsitéattMunchen，October2003.[7] DIMACS满意度建议格式，1993年。获取网址ftp://dimacs.rutgers.edu/pub/challenge/satisfiability/doc网站。[8] Nikla s E'en and Nikla s Séorenson.一个简单的S AT解决方案。InEnr icoGi un ch igliaand ArmandoTacchella ， editors ， Theory and Applications of Satifiability Testing ， 6th InternationalConference，SAT 2003. Santa Margherita Ligure，意大利，2003年5月5-8日，精选修订论文，计算机科学讲义第2919卷，第502-518页。Springer，2004.[9] Pascal Fontaine，Jean-Yves Marion，Stephan Merz，Leonor Prensa Nieto和Alwen Tiu。表现力+自动化+可靠性：将SMT求解器和交互式证明助手相结合。QSL Loria，2005年10月。[10] 埃夫格尼·戈德堡和雅科夫·诺维科夫。CNF公式的不满足性证明的验证。在欧洲的设计、自动化和测试（日期2003），第10886IEEE计算机学会，2003年。[11] M. J. C.戈登从LCF到HOL：一个简短的历史。 In G. Plotkin，Colin P. Stirling，Mads Tofte，编辑，Proof，Language，and Interaction。麻省理工学院出版社，2000年。[12] M. J. C. 戈登HolSatLib文档，版本1.0b，2001年6月。获取网址http://www.cl.cam.ac.uk/http：//www.example.com[13] M. J. C. Gordon和T. F.梅勒姆编辑们HOL简介：高阶逻辑的定理证明环境。剑桥大学出版社，1993年。[14] H.lgerH. 你和你的妈妈都很好。 SATLIB：AnonlinereurceforresearchonSAT.IanGent、Hansvan Maaren 和 Toby Walsh 编 辑 ， SAT 2000 ， 第 283-292 页 。 IOS Press ， 2000. 可 在www.example.com上在线获取http://www.satlib.org/。[15] 乔·赫尔·德。 我不喜欢吃鸡蛋和鸡蛋。InYvesBertot，GillesDowek，AndrsHirschowitz，ChristinePaulin ， andndLarentThry ， editors ， TheremProvinginHigherOrderLogics ，12thInternational Conference，TPHOLs斯普林格。[16] 乔·赫德。HOL和一阶逻辑之间的LCF风格接口。在Andrei Voronkov，编辑，Proceedings of the18th International Conference on Automated Deduction （ CADE-18 ） ， Volume 2392ofLecture Notes in Arti Ficial Intelligence，pages 134斯普林格。[17] R. Kumar，T. Kropf和K.施耐德在HOL环境中集成一阶自动证明器。In M.作者：J. J. N. Levitt和P. J. Windley 编 辑 ，1991 年 HOL定 理 证明 系 统 及其 应 用 国 际研 讨 会 论 文集 ， 第170IEEEComputer Society Press，1992.[18] 贾梦。交互式和自动校准器的集成。Manuel Carro和Jesus Correas，编辑，关于计算逻辑系统实现技术的Second penalty Net Workshop，2003年9月。T. Weber/Electronic Notes in Theoretical Computer Science 144（2006）6779[19] Jia Meng 和 Lawrence C. 保 尔 森 使 用 解 析 支 持 交 互 式 证 明 的 实 验 。 IinDavidBasinanddMichaéelRusinowitch ， editors ， AutomartededdReasoning ： SecondInternationalJointConference，IJCAR 2004，Cork，Ireland，July 4-8，2004，Proceedings，volume3097ofLecture Notes in Arti ficial Intelligence，pages 372Springer，2004.[20] M.莫斯凯维奇角Madigan，Y.赵湖，加-地Zhang和S.马利克 Cha Cha：Engineering an efficientSAT solver.第38届设计自动化会议论文集，拉斯维加斯，2001年6月[21] 放大图片作者：Tobias Nipkow，Lawrence C.保尔森和马库斯·温泽尔。Isabelle/HOL -施普林格，2002年。[22] S. Owre，J. M. Rushby和N.史恩卡PVS：原型验证系统。 在Deepak Kapur，编辑，第11届自动演绎国际会议（CADE），人工智能讲义第607卷，第748-752页，萨拉托加，纽约，1992年6月。斯普林格。[23] 劳伦斯角，澳-地保尔森Isabelle：A Generic Theorem Prover，计算机科学讲义第828卷。Springer，1994年。[24] 劳伦斯角，澳-地保尔森一个通用的tableau prover及其与Isabelle的集成。Journal of UniversalComputer Science，5（3）：73[25] 纳塔拉詹·香卡使用高阶逻辑的决策过程。在Richard J. Boulton和Paul B. Jackson，编辑，Theorem Proving in Higher Order Logics ， 14th International Conference ， TPHOLs2001，Edinburgh，Scotland，UK，September 3-6，2001，Proceedings，Volume 2152ofLecture Notes in Computer Science，pages 5Springer，2001年。[26] 奥弗·斯特里克曼用SAT解Presburger和线性算术。 In M. D. Aagaard和J. W. O’Leary, editors, 施普林格，2002年。[27] 吉 欧 · 萨 特 里 和 克 里 斯 蒂 安 · 苏 特 纳 。TPTP 问 题图 书 馆 ：CNF发 布 v1.2.1 。JournalofAutomatedReasoning，21（2）：177-203，1998.可在http://www.cs.miami.edu/httptp/上查阅。[28] G. S.蔡廷 论命题演算中推导的复杂性。 在J. Siekmann和G. Wrightson，editors，AutomationOf Reasoning ：Classical Papers On Computational Logic ， Vol. II ， 1967-1970 ， pages466-483. Springer，1983年。也在结构在建设性数学和数理逻辑第二，编辑。A. O. Slisenko，1968，pp.115-125[29] Tjark Weber. Isabelle/HOL的有界模型生成。Wolfgang Ahrendt，Peter Baumgartner，Hans deNivelle，Silvio Ranise，and Cesare Tinelli，editors，Selected Papers from the Workshops onDisproving and the Second International Workshop on Pragmatics of Decision Procedures（PDPAR 2004），volume 125（3）ofElectronic Notes in Theoretical Computer Science，pages 103-116. Elsevier，2005年7月。[30] 张林涛和沙拉德·马利克。使用独立的基于分辨率的检查器验证SAT解算器：实际实现和其他应用。 在欧洲的设计、自动化和测试（日期2003），第10880IEEE计算机学会，2003年。