集成验证系统：Isabelle、Maple和QEPCAD的验证者

可在www.sciencedirect.com在线获取理论计算机科学电子笔记285（2012）115-119www.elsevier.com/locate/entcs围绕用户集成系统：在验证器中结合Isabelle、Maple和QEPCAD劳拉岛Meikle1 雅克·D Fleuriot2爱丁堡大学信息学院英国摘要我们描述了证明者的验证，一个通用的，模块化的架构，结合工具的正式验证，与关键differentiator的集成强调的作用，用户。结合定理证明器Isabelle与计算机代数系统Maple和QEPCAD-B的具体实现。这说明证明器的设计原则关键词：定理证明，计算机代数，UI，Isabelle，Eclipse，QEPCAD，Maple。第一章证明者的简介今天的交互式定理证明允许验证复杂的定理和复杂的算法，尽管这个过程仍然繁琐和耗时。我们相信，在许多情况下，使用其他工具，如计算机代数系统（CAS），可以加速这一进程。虽然在将证明器与外部工具相结合方面取得了重大进展，如先前的工作[6]所述，但当前证明开发的复杂性增加对工具集成提出了新的要求和挑战我们首先假设集成到目前为止，这主要是通过集成来实现的，集成可以自动简化表达式并实现子目标[8][11]。随着更复杂的验证任务-以及更多的数学家使用1电子邮件：lauram@dai.ed.ac.uk2电子邮件：jdf@inf.ed.ac.uk1571-0661 © 2012由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2012.06.010116L.I. Meikle，J.D.Fleuriot/Electronic Notes in Theoretical Computer Science 285（2012）115证明器-我们相信，形式证明的过程也可以从工具集成中受益为了实现这一点，重要的是集成支持多种交互模式：用户应该可以选择以完全自动化的方式使用外部系统，但他们也应该可以选择修改该系统的使用方式。新手用户可以从各种证明助手中受益，即使他是不熟悉这些工具的用户可以使用这些工具，而专家用户则可以访问这些工具的全部丰富内容。对于某些问题来说，这可能是必不可少的，因为即使是最好的全自动集成也不能总是适当地调整参数此外，通过允许工具集成的更多方面的可见性和可修改性，用户在探索问题时具有更大的灵活性。我们相信，半交互式集成框架现在扮演着至关重要的角色：框架应该支持自动配置适合特定问题的设置，但也要强调探索和更改这些值的可用性，同时保持系统之间的一致性这一理念引导我们开发了Prover结合Isabelle和QEPCAD-B的具体实现，帮助用户推理实非线性多项式，已经实现[6]。 在本文中，我们将我们的方法应用于进一步的系统集成，以表明设计原则适用于更普遍的，我们的架构可以很容易地扩展到支持更多的工具。特别是，我们将Maple [10]集成到Prover的数据库中，并展示其绘图功能如何为被证明的定理提供重要的洞察力。我们的框架可以在www.cognetics.org/proverspalette。2系统设计我们的方法的关键思想是通过一个有凝聚力的用户界面（UI）来统一多个工具，允许在证明过程中的任何时候使用任何相关的工具。这是通过为每个外部工具构造UI“View”小部件来实现的。这些视图位于IDE中的校样脚本旁边，并且：• 当证明状态发生变化时，框架会通知每个视图，并适当更新，自动获取其母语的翻译和适当的默认设置选择。• 每个视图都可以被配置为在“新手”模式下运行• 通过显示可选的“选项卡”序列• 每个视图都以集成的形式呈现外部系统的计算结果L.I. Meikle，J.D.Fleuriot/Electronic Notes in Theoretical Computer Science 285（2012）115117我们已经在Java中实现了这种设计，使每个视图都成为Eclipse Proof GeneralKit的插件[1]，利用其代理结构，并针对Isabelle定理证明器[9]。Prover的该实现提供了抽象超类，这些超类封装了常见功能，包括定义视图和选项卡，跟踪和转换证明状态，在必要时修改证明状态（例如扩展定义，转换为PNF），以及以各种方式插入结果（通过oracle，通过实例化等）。这最大限度地减少了将新工具与Prover的扩展集成所需的额外代码接下来我们通过描述我们的实现来证明这一点，该实现将Maple支持添加到我们的系统中。3使用Maple在Prover图1. 使 用 证明者的工具进行推理：IDE中的Isabelle、QEPCAD和Maple由于Maple是一个功能强大且受欢迎的CAS，我们选择将其集成到证明者的眼睛 我们通过以下方式来说明我们的方法和这种集成 一个使用Maple绘图功能的真实示例。图1显示了带有新Maple视图的proverIDE图1中的证明脚本重新访问了Collins和Hong [3]描述的冲突问题。这涉及到机器人运动规划和查询是否移动的圆（1）和移动的正方形（2）会发生碰撞，特别是询问是否txy.t≥0<$（1）<$（2）：3. The Prover118L.I. Meikle，J.D.Fleuriot/Electronic Notes in Theoretical Computer Science 285（2012）11516161717(1)（x−t）2+y2≤1（2）−1≤x−17t≤1− 9≤y−17t≤−7仅仅依靠一个定理证明器，这可能是一个困难的证明，使用者必须解决从如何应用无数引理到对象是否被正确定义以及定理是否可证明的问题枫木可以对后两者给予肯定 使用Prover的Probe，MapleView会不断更新以反映当前的proof目标状态：例如，用户可以选择绘制这些方程（在MapleView的“Problem”选项卡上，如图1所示）。 积分自动转换问题-剥离量化器，打破连接，转换不等式-然后确定哪些方程适 合 包 含 ， 以 及 哪 种绘 图 类 型 和 命 令 是 适 当 的（ 例 如 ， ImplicitPlot ，ImplicitPlot3D，animate）4.对于碰撞问题，Maple集成默认为2D动画。它自动确定了每个轴的变量，并推断出六个组成方程中的五个应该被绘制出来。 在这个情节配置中，t= 0没有意义;但是用户可以自由地更改变量到轴的映射，如果t和x交换-这样t就沿着x轴绘制，我们可以在时间x上进行动画-那么启用的方程列表将更新为包括t= 0，尽管图可能不直观！用户可以选择按钮将绘图命令发送到Maple。或者，用户可以转到此选项卡还允许随时取消外部流程。要求Maple绘制碰撞问题会导致一个新窗口，其中包含圆形和正方形随时间移动的交互式动画。图2显示了这个动画的一个静态，其中圆形和正方形正在碰撞，证实了这个问题是可证明的。图2. 枫叶动画情节在Maple命令的视觉洞察之后，用户还可以在Prover的可编程环境中调用QEP-CAD。之前我们展示了如何使用QEPCAD来确认问题是“真”的它还可以生成证人（t=96，x=96和y=-1），集成可以将其实例化到证明中，一次点击4由于空间限制，这里不包括自动转换和配置，使问题适合使用Maple感兴趣的读者可以参考[7]。L.I. Meikle，J.D.Fleuriot/Electronic Notes in Theoretical Computer Science 285（2012）1151194结论通过将Maple集成到Prover的SDK中，我们已经表明该框架可以推广到支持其他外部工具。进一步扩展该系统以支持其他定理证明器将是很有意思的，这些定理证明器可以与PG Kit兼容;随着新的基于Java的证明器IDE（如I3 P）的出现，[4]，我们相信我们的制度有希望实现更广泛的一体化。我们还表明，一个交互式的集成框架是能够提高用户的理解证明问题。这支持了我们的假设，即当一个紧密集成但可定制的工具面板方便地供用户使用时，用户的权力最大。一个成功的集成框架可以更深入地理解证明义务，将用户从繁琐、平凡的证明细节中解放出来，但不会过度限制可能的内容确认我们要感谢评论者提出的有益意见。这项工作由EPSRC赠款EP/E005713/1资助。引用[1] AspinallD.，C. Lu¨th和D. Winterstein，一个用于交互主动生产的框架. TowardsMechanizedMathematical Assistants，Springer LNAI 4573（2007），161-175.[2] 布朗角W.，QEPCAD B：使用CAD计算半代数集的程序，SIGSAM Bulletin，37（2003），97-108。[3] 柯林斯湾E、和H. Hong，Partial Cylindrical Algebrical Decomposition for Quantifier Elimination，Journal of Symbolic Computation12（1991），299-328.[4] GastH、I3P，www-pu.informatik.uni-tuebingen.de/i3p[5] 赫内费尔德A.，Using Features for Automated Problem Solving，PhD Thesis，University ofEdinburgh，2007.[6] 米克尔湖一、和j.d. Fleuriot，Combining Isabelle and QEPCAD-B in the Prover[7] 米克尔湖一、几何算法的形式验证，以博士论文的形式出现，大学爱丁堡。[8] 孟杰，C. Quigley和L. C. Paulson，Automation for Interactive Proof：First Prototype，Inf. 计算：204：10（2006），1575-1596.[9] 保尔森湖 C.的方法， Isabelle：A Generic Theorem Prover，LNCS828（1994）.[10] Redfern M.，和D. Betounes，[11] 蒂瓦里A. PVS-QEPCAD，www.csl.sri.com/users/tiwari/qepcad.html。