结合HOL-Light和CVC Lite的协同定理证明器

理论计算机科学电子笔记144（2006）43-51www.elsevier.com/locate/entcs协同定理证明器：结合HOL-Light和CVCLite肖恩·麦克劳克林 克拉克·巴雷特b 叶挺葛ba卡内基梅隆大学计算机科学系，seanmcl@cmu.edu纽约大学计算机科学系，{barrett，yeting}@ cs.nyu.edu摘要本文是一个结合定理证明器的案例研究。我们在HOL-Light中定义了一个派生规则CVC PROVE，它调用CVC Lite并将生成的证明对象转换回HOL-Light。因此，我们为CVC Lite获得了高度可信的校对器，同时也从根本上扩展了HOL-Light的功能。保留字：HOL，CVC，定理证明，证明检验1介绍和历史定理证明进展的一个重要障碍是，在不同的定理证明者之间共享结果通常是困难的。解决这个问题的一个尝试是新生的Logosphere项目[1]。这有望成为一个不同格式的定理数据库，具有各种逻辑之间的系统翻译机制[8]。另一个例子是可以导入其他一些系统（例如：TPS），并使用其他定理证明在某些领域（如搜索证明）。Otter [3] for first order logic）。另一个困难来自于不同的定理证明者对证明和正确性的重视程度不同。使用不可信的外部证明器作为预言机可能会损害可靠性，这在大多数情况下是不可接受的。HarrisonanddTh′ery[11]describeaso-called1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.12.005B44S. 麦克劳克林及其他人/理论计算机科学电子笔记144（2006）43喂。在鼓励沿着这些路线进一步取得进展的希望，本文介绍了一个案例研究，使用“怀疑论”的方法，其中自动定理证明器CVC建兴生成的证明条款被翻译成相应的证明在互动定理证明器HOL光。虽然一般的方法并不新鲜，但这种特殊的定理证明器耦合带来了独特的挑战和好处。HOL-Light是一个具有非常小的可信核心的通用定理证明器。相比之下，CVC Lite采用了更务实的方法，从而产生了更大的可信核心。通过连接两个校准器，HOL-Light能够利用CVC Lite 与此同时，透过使用HOL-Light作为校对员，我们对CVC Lite所得结果的信心可大幅增加。在简要描述了每个系统之后，我们解释了实现以及将证明从CVC Lite转换为HOL-Light所需的内容。然后，我们给出了一些结果，包括一类问题，可解决的HOL-轻使用CVC证明，但无法解决，否则。其他不太成功的例子是为了比较。 我们还展示了如何在CVC Lite的帮助下将阵列理论轻松添加到HOL-Light。最后，我们讨论了潜在的应用和未来的工作。1.1HOL-LightHOL-Light [9]是一个交互式定理证明器，它起源于LCF项目[7，13]和HOL 4定理证明器[4]。所有的定理都是由一组核心的10个原始推理规则，如肯定前件和相关性。这些推理规则在OCaml语言中实现为函数。其他的推理规则（称为派生规则）是从这些原始规则中保守地派生出来的。它们是保守的，因为它们只包括原始规则的日益复杂的应用，因此不会扩大系统的力量。使用OCaml，用户可以编程新的规则（例如，（三）不损害制度的健全性。核心由大约1500行OCaml组成。HOL-Light已被其作者广泛用于验证英特尔的浮动点算法[10]。大量的数学已经在系统中形式化，从实数的构造到transfinite集合论和实复分析的基本结果。S. 麦克劳克林及其他人/理论计算机科学电子笔记144（2006）43451.2CVC精简版CVC Lite [5]是一个用于可判定一阶理论的自动证明生成定理证明器。它源自斯坦福大学的SVC和CVC项目[6，14]。逻辑核心在许多方面与HOL-Light内核不同。例如，由于速度是系统的设计目标，因此CVC Lite中有更多的原始推理规则实际上，仅实数线性算术理论就有一百多条（将这个数字与HOL-Light的10个总推理规则进行对比，其中实数是从无限性公理构建的可信代码库相应地更大，超过3000行用于解决线性实数运算问题2执行证明在CVC Lite中表示为树状数据结构1。节点标记有推理规则的名称和该规则的参数。这些参数可以是类型、项或其他证明对象。 我们为每个CVC Lite推理规则实现HOL-Light派生规则，并首先转换证明树深度，当遇到每个CVC Lite规则时调用相应的HOL-Light规则。(An示例如下。）因此，CVC Lite中的错误不会损害HOL-Light系统。CVC Lite生成的错误证明根本无法转换为HOL-Light。2.1翻译类型和术语鉴于CVC Lite逻辑接近于HOL-Light逻辑的子集，翻译类型和术语是简单的。 每个系统都有布尔类型和实类型的概念。CVC中的术语是一阶的，是HOL-Light高阶对象语言的子语言因此，翻译术语也很容易2.2翻译校对CVC Lite中的证明是Curry-Howard Iso- morphism意义上的证明项[12]。证明本身直接对应于一个简单的函数程序。因此，翻译过程可以看作是在HOL-Light中执行此作为一个例子，下面是CVC Lite的证明格式中的命题q1唯一的并发症是变量绑定。46S. 麦克劳克林及其他人/理论计算机科学电子笔记144（2006）43(iff_transs（NOT（p => q），NOT（NOT p OR q），（p AND NOT q），basic_subst_op（NOT（p => q），NOT（NOT p OR q），rewrite_implies（p，q）），rewrite_not_or（NOT（NOT p OR q）CVC Lite的证明格式是一个类似于Lisp的派生树表示，最外面的表达式表示树的根。树的每个节点都是推理规则的应用，它的子节点是推理规则的参数或前提。该证明使用以下四个推理规则2（一）► （α→β）参与（<$α<$β）重写意味着（α，β）► α↔β（二）► φ[α]参与φ[β]基本取代基（α，β）（三）► <$（α<$β）参与（<$α<$β）重写not或（<$（α<$β））► α↔β►β↔γ（四）► α↔γ当且仅当transs（α，β，γ）请注意，每个推理规则都有一个或多个参数。在CVC Lite生成的派生树的表示中，特定节点处的这些参数的值取自该节点的前几个子节点。节点的其余子节点是推理规则（如果有的话）的前提的派生树。相应的证明树看起来像这样（为了清楚起见，省略了推理规则► （p→q）参与（<$p<$q）► <$（p→q）参与<$（<$p<$q）（一）（二）► q）（三）（四）► q）S. 麦克劳克林及其他人/理论计算机科学电子笔记144（2006）4347[2]通常，横杠下面的表达式代表结论，横杠上面的表达式代表前提。48S. 麦克劳克林及其他人/理论计算机科学电子笔记144（2006）43为了将这些证明项转换为HOL-Light，我们为证明树中遇到的每个CVC Lite规则提供了一个HOL-Light因此，翻译对应于功能应用。在CVCLite中，我们为每个推理规则都设置了一个规则。然后，我们将这些规则结合在一个递归过程中，该过程将证明转换为证明树的深度优先遍历。如果没有错误，根证明节点的平移产生所需的HOL-Light定理。3结果我们专注于两类可由HOL-Light和CVC Lite解决的问题：布尔满足公式和实数算术公式。3.1布尔可满足性为了评估在HOL-Light中使用CVC PROVE进行布尔可满足性的有效性，我们研究了众所周知的鸽子洞问题：给定n−1组n个鸽子洞，排列在n行n−1列中，并且没有一列可以包含超过一只鸽子，找到与断言相矛盾的地方。每一排都能放一只鸽子对于n= 3，相应的布尔满足性公式为：（<$x1x3）（<$x1x5）（<$x3x5）（<$x2x4）（<$x2x6）（<$x4x6）（x1x2）（x3x4）（x5x6）。对于典型的布尔可满足性方法来说，这是一个非常困难的问题下面的表3给出了CVC Lite单独运行（但仍产生校样）、HOL-Light单独运行以及HOL-Light使用CVC Lite并执行翻译的时间。3所有时间均以秒为单位，运行在运行FreeBSD 5.2的1GH Pentium IIIS. 麦克劳克林及其他人/理论计算机科学电子笔记144（2006）4349nCVC精简版HOL-LightCVC证明20.104.51.7530.18131040.90344352.9*210619*9807238*4308“HOL Light”下的空条目在该系统中是难以处理的。即使是n= 5的例子，在我们杀死进程之前也运行了4个多小时因此，我们使用外部系统CVC Lite扩展了HOL-Light的功能3.2实数算术我们在翻译过程中研究的第一个问题是实线性算术项。当时，霍尔-莱特的决策程序“真实的阿里斯”非常缓慢。使用CVC PROVE在这些问题上往往会产生良好的速度改善，通常是未辅助的REAL ARITH的2到3倍。Hol-Light的作者John Harrison后来优化了REAL ARITH。使用新的算法程序，CVC PROVE的速度大约慢六倍。在这种情况下，优化原始决策过程比使用外部工具更有效4数组理论上面记载的实验来自于存在于两个定理证明者中的理论。翻译的一个更有趣的应用是那些在证明者中还不存在决策程序的理论。例如，CVCLite有一个很好的数组理论。这个理论在当前的HOL-Light版本中不存在。作为在HOL-Light中实现数组决策过程的替代方案，我们扩展了当前的翻译机制来处理CVC Lite数组推理规则。使用CVC Lite理论所需的全部HOL-Light这给了我们所有的权力，一个霍尔光阵列理论与最小的电子束。50S. 麦克劳克林及其他人/理论计算机科学电子笔记144（2006）434.1理论该理论是一个简单的阵列扩展理论，如[15]所示有两个功能符号，读和写。该理论公理化如下：（i=j→（读（写a i v）j）=v）（i j→（read（writea i v）j）=（reada j））（（i. （读a i）=（读b i））→ a = b）4.2结果考虑下面的公式，其中a和b是数组：（a=b）→（写a i（读b i）=a）给定公理，内置的HOL-Light一阶推理器可以在56秒内解决这个问题CVC PROVE需要0.015秒。即使是稍微困难的问题，如以下是棘手的HOL-Light。相比之下，CVC PROVE在7.6秒内解决了这个问题。(((写a i v=写b j w）（读a i=v）（读b j=w））→（（a=b）<$（（i=j）→（v=w））<$（（i j）→读a j=w））5未来研究有一个广泛的证明理论文献证明压缩。这些都不是目前适用于CVC精简版的证明。此外，对于更大的问题，可能需要将证明翻译成片段，以允许整个对象适合内存。另一个方向是允许两个证明者之间进行更多的互动。目前，除了一个单一的证据之外，没有任何信息交流。一种可能性是允许HOL-Light决策过程在证明搜索期间尝试解决子目标时自动调用CVC Lite。6结论这项工作证明了可以从组合定理证明器中获得的几个好处。我们通过翻译CVC Lite的证明，展示了HOL-Light的能力得到质的提升的具体例子。另一方面，我们还发现了一个优化决策过程的例子，S. 麦克劳克林及其他人/理论计算机科学电子笔记144（2006）4351直接在HOL光优于进口证明从CVC建兴。因此，我们不得不考虑使用其他工具所获得的权力是否值得。在布尔可满足的情况下，这种组合无疑是成功的。在改进SAT求解器方面，大量的改进来自于使用先进的算法和数据结构，以实现通过布尔搜索空间的更快搜索。在像HOL Light这样的系统中模仿这一点将花费相当大的时间，并且仍然会遇到搜索本身比用低级语言编写并针对速度进行优化的工具慢的问题。使用一个快速的工具来找到证明，然后将证明转换为HOL-Light似乎是有意义的。在实数运算的情况下，几乎没有搜索，实际算法非常相似，直接在HOL Light中优化是一个更好的解决方案。在阵列的情况下，HOL Light中不存在的理论，CVC Lite中存在的决策过程很容易并且立即有用。组合定理证明器的一个目标是在新的上下文中提供价值，而不必重复人类的工作。第一和第三个例子充分证明了这一点我们希望这项工作将激励额外的努力，以结合定理证明。7致谢我们我们引用[1] http://www.logosphere.org网站。[2] http://www.ags.uni-sb.de/www.example.com[3] http://www-unix.mcs.anl.gov/AR/otter/网站。[4] http://hol.sourceforge.net/网站。[5] C. Barrett和S. Berezin CVC Lite：一种新的协作有效性日检查员。In R.Alzheimer和D.A. Peled，编辑，第16届国际会议计算机辅助验证（CAVSpringer-Verlag，2004年7月。马萨诸塞州波士顿[6] C. W. Barrett，D. L. Dill和J. R.莱维特对具有平等性的理论组合进行有效性检查。In M.Srivas和A.卡米莱里，编辑，第一届国际会议52S. 麦克劳克林及其他人/理论计算机科学电子笔记144（2006）43计算机辅助设计中的形式方法（FMCADSpringer-Verlag，Nov. 1996.加州帕洛阿尔托[7] M.戈登河Milner，和C. P.沃兹沃斯爱丁堡LCF：一个机械化的计算逻辑。在计算机科学讲义中，第78卷。Springer-Verlag，1979.[8] R. Harper ， F. Honsell 和 G. 普 洛 特 金 定 义 逻 辑 的 框 架 。 在 Journal of the Association forComputing Machinery（JACM），第40卷，第143-184页[9] J·哈里森HOL light：Atutorial introduction. In M. Srivas和A. Camilleri，编辑，计算机辅助设计形 式 方 法 第 一 次 国 际 会 议 论 文 集 （ FMCADSpringer-Verlag ， 1996. 参 见http://www.cl.cam.ac.uk/users/jrh/hol-light。[10] J·哈里森三角函数的形式验证。 In W. A. Hunt和S. D. Johnson，editors，Formal Methods inComputer-Aided Design ： Third International Conference FMCAD 2000 ， Volume 1954ofLecture Notes in Computer Science，pages 217Springer-Verlag，2000.[11] J. 我的名字叫HArison and L. 你好。一家专业的公司为客户提供专业的服务。自动推理的基础，21：279[12] W. A.霍华德公式作为类型的构造概念。第479-490页。中国科学技术出版社，1998年.[13] L.保尔森逻辑与计算：剑桥LCF交互式证明。在剑桥Tracts in Theoretical Computer Science，第2卷。剑桥大学出版社，1987年。[14] A.施通普角W. Barrett和D. L.迪尔 CVC：一个合作的有效性检查器。在大肠布林克斯马日和K. G. Larsen，编辑，Proceedings of14计算机辅助设计验证（CAVSpringer-Verlag，2002年7月。 丹麦哥本哈根[15] A. Stump，D.L. 迪尔角，澳-地W. Barrett和J.莱维特一个扩展的决策过程数组理论第16届IEEE计算机科学逻辑研讨会论文集（LICSIEEE计算机学会，2001年6月马萨诸塞州波士顿