动态几何软件与证明助手的交互式形式证明系统-理论计算机科学电子笔记285（2012）43-55

可在www.sciencedirect.com在线获取理论计算机科学电子笔记285（2012）43-55www.elsevier.com/locate/entcs结合动态几何软件和证明助手的交互式形式证明范端明1Yves Bertot2Inria Sophia Antipolis摘要本文提出了一种几何证明接口它是一个动态几何软件Geogebra[11]与证明助手Coq[8]的组合由于Geogebra的功能，用户可以创建和操作几何结构，他们发现几何图形，并在Coq的支持下交互式地构建形式证明。我们的系统允许用户构建完全传统的证明，在高中的风格相同。对于证明的每一步，我们为用户提供了一组在Coq中验证的适用规则，我们还提供了Coq中的策略，通过这些策略，自动解决了推理的小步骤关键词：交互式几何证明，Coq，证明助手，动态几何1引言动态几何软件在当今数学教育中发挥着重要的作用，对数学教育有着很大的促进作用。学生可以用它来构建几何对象，观察这些对象如何改变时移动自由点或应用欧几里德变换，他们可以发现插图。市场上有许多具有各种功能的交互式几何应用程序，其中许多应用程序在许多国家的课堂上得到了实际应用然而，这些用途通常局限于发现文物的水平。一些DGS通过与自动几何定理证明（GTP）相结合，提供证明功能，允许用户验证图形。它们依赖于几种有效的自动证明方法，如Gr？obner基方法[13]、Wu前两种方法是使用多项式来解决问题的代数方法，它们不能给我们人类可读的证明。最后两个可以1电子邮件：tuan-minh. sophia.inria.fr2电子邮件：Yves. inria.fr1571-0661 © 2012由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2012.06.00544T.M. 范，Y。Bertot/Electronic Notes in Theoretical Computer Science 285（2012）43产生人类可读的证明，然而这些证明不是完全传统的证明，它们不依赖于高中教授的几何知识我们的目标是为学生建构一个互动式的几何定理证明工具.学生们可以按照高中的教学方式一步一步地推理。这种风格可能涉及向后和向前证明推理，也可能涉及辅助线的构建。本文提出了一个将Geogebra与Coq相结合的交互式几何证明接口GeoCoq。推理步骤通过鼠标点击构建并发送到Coq。就其本身而言，Coq执行推理步骤，响应被发送回用户以继续他们的证明。逻辑步骤和知识是由一个图书馆，这是与高中教师的帮助下开发的。在Coq这样的证明助手的支持下，推理步骤得到了验证，证明的正确性得到了保证。这是使用Coq的一个优势，因为几何推理通常使用基于视觉证据的默认假设，而无需验证。我们还开发了自动化的策略，帮助用户解决小步骤的reasoning。 用户不必深入研究导致技术证明的细节，也不必适应他们的抽象级别。 此外，随着正规化 Coq中的自动证明方法（如J.Narboux [14]形式化的面积方法），用户可以使用这些方法在证明之前检查事实，或者在构造证明的步骤中使用它们本 文 的 组 织 结 构 如 下 。 在 第 二 节 中 ， 我 们 给 出 了 一 个 简 短 的 描 述 关 于Geogebra。第3节描述了Coq系统、使用Pcoq的通信以及关于几何库的简要描述。第4节介绍了接口和提供的功能证明。下一节将介绍我们的实现。第六节介绍了相关的工作，最后一节是结论和展望。2地质Geogebra是一个免费的动态几何软件，用于学校教育。它由Markus Hohenwarter于2001年在他的硕士和博士工作中开始[11]。它是用Java实现的，因此可用于多种平台。它将几何、代数和微积分有机地结合起来，为数学提供了一种新的工具它获得了多个国际教育软件奖项，并被应用于不同国家的学校教育。像其他动态几何系统一样，Geogebra提供基本的几何对象，如点，矢量，直线，圆，以及更复杂的结构，如中点，平行线，外接圆。. .用户可以构造几何对象并操纵它们。Geogebra还允许学生在任何时候撤销或重做构造。通过移动五个自由点，学生可以找出表达式并检查其正确性，目前检查仅限于两个对象动态几何与计算机代数系统（CAS）的联系是Geogebra区别于其他动态几何系统的一个重要方面GeoGebraT.M. 范，Y。Bertot/Electronic Notes in Theoretical Computer Science 285（2012）4345可以受益于CAS的可视化功能和DGS的动态可变性。它鼓励学生以双向实验的方式发现数学学生可以研究对应于绘制对象的方程，也可以研究对应于给定方程的数字通过结合Geogebra和Coq，我们希望提供一个界面，让学生有许多观点的几何问题。3Coq通信和几何库Coq是一个证明开发系统，它允许用户定义函数或预测，陈述数学定理并交互式地开发形式证明。Coq不是一个自动定理证明器，但是它提供了一种策略语言，让用户定义自己的证明方法，它还包括自动定理证明和决策过程的策略。所以Coq适合我们交互式构造证明的需要。一些集成开发环境（IDE）可以用来与Coq通信。在这里，我们感兴趣的是Pcoq，它是Coq的图形用户界面[1]。使用Pcoq与Coq进行通信可以带来一些好处。Pcoq是在Java中实现的，Java是与Geogebra相同的编程语言，因此这使得它很容易集成到Geogebra中。Pcoq将所有公式和命令作为树状结构（也称为抽象语法树）而不是纯文本进行操作。这使得在某些函数上附加特殊的数学符号，以及在几何陈述上附加自然语言的句子变得容易。此外，这为我们从Coq接收到的信息结构（假设，目标）提供了一个简单的访问。为了能够在Coq中进行推理，我们还需要一个几何库，在其中形式化几何基本概念及其属性，验证我们想要提供给用户的几何规则。F.Guilhot为法国高中课程开发了一种有趣的形式化[12]。它的基础是提供一个新的公理系统，更适合学生的知识。它涵盖了平面几何的大部分基本概念，性质和定理。此外，证明是传统的，他们是形式化的推理方式适合高中学生的能力。其中的经典定理证明，在这个图书馆，我们可以引用墨涅拉俄斯，塞瓦，笛沙格，毕达哥拉斯，西姆森. .4接口我们的界面是Geogebra与Pcoq的结合。我们将Pcoq整合为Geogebra的视图（图1）。像其他视图一样，它可以显示、隐藏、拖动以修改其位置，以及作为外部窗口打开Pcoq的两个主要子窗口是命令窗口和验证窗口。命令窗口用于显示所有陈述和证明定理的Coq命令。证明窗口允许用户构造证明，他们可以看到假设，目标需要证明几何推理的每一步。46T.M. 范，Y。Bertot/Electronic Notes in Theoretical Computer Science 285（2012）43图1.一、GeoCoq GUI的屏幕截图Pcoq被集成为左边的窗口此外，其他子窗口用于显示适用于目标的规则，通过为其参数提供值来应用规则，以及通知错误。. . 我们详细的界面和它的功能，显示用户如何可以状态和证明定理。下面的定理将被用作本节其余部分的示例例4.1设BD和CE为三角形ABC的两个高度，G点和F点分别为BC和DE的中点它认为，GF的。4.1陈述定理4.1.1构造图Geogebra为用户提供了通用的几何构造工具来构造图形。通过使用适当的构造工具并选择现有对象，可以逐个创建几何体对象。用户可以移动自由点，并且依赖结构将被更新，这可以帮助用户发现结构。为了构造与上述示例相对应的图，用户绘制三角形ΔABC，构造垂直线d<$ AC使得B∈ d和e<$ AB使得C∈ e，取交点E和D，并通过分别取BC和DE的中点G和F并将它们连接来完成图形。每个构造都被翻译成Coq中的命令（图1）。添加新的几何对象或移除现有几何对象意味着添加或移除相应的假设。在大多数几何定理证明器中，几何命题都是用谓词形式来描述的，即谓词形式.假设和结论由几何谓词表示我们的工具也不例外，但是在陈述定理的阶段，我们有构造形式的几何陈述（表1的左列）。在定理证明阶段（将在下一节介绍），用户可以T.M. 范，Y。Bertot/Electronic Notes in Theoretical Computer Science 285（2012）4347使用我们在Coq中的策略来展开假设中的定义，获得相应的几何谓词（表1构成形式谓语形式M =中点（A，B）共线（A B M）<$MA = MB M =交点（l1，l2）l1<$l2<$M∈l1< $M∈l2l = line（A，B）A = B<$ A∈ l< $B∈ l l =parallelLine（A，m）A∈ l<$ l<$ ml =奇异线（A，m）A∈ l <$l<$ m表1某些构式4.1.2发现艺术品一旦一个图表被完全构建，用户很容易看到不依赖于其他结构的自由点，因为这些点使用不同的颜色突出显示用户可以通过拖放来移动这些自由点，更新相关结构，并且用户可以观察几何对象之间的关系，点的轨迹。. .如果他们看到一个猜想似乎是正确的，他们可以决定证明它。我们可以预先验证猜想的正确性，以确保用户将证明一个事实。这种预验证可以使用Geogebra特性在CAS的支持下进行，或者使用Coq中的自动证明方法（例如面积方法）。对于我们的例子，用户可以移动点A，B和C，他们找到GF和DE的相似性（GF DE）。他们选择这些行并右键单击，出现一个对话框来确认这种相似性，并要求用户证明它（图2）。一旦用户决定证明猜想，我们就可以进入下一节的定理证明阶段。4.2定理证明我们从发现结构中的几何谓词开始这一节我们的实现允许用户自动或手动获得几何谓词用户可以在假设中选择一个几何对象定义，并使用鼠标点击获得其属性，他们也可以同时展开假设中的所有定义相应的战术会自动发送给Coq。下面的策略收集定义新点的假设（如M是直线a和b的交点），并创建新的假设来枚举新点的给定属性（如M∈ a，M∈ b和a∈ b）。LTACn r o l l所有定义：=匹配戈阿勒 与|H: ? M =交点？一？B|−=>>最大值l e t H1 H2 H3：= f r e s h48T.M. 范，Y。Bertot/Electronic Notes in Theoretical Computer Science 285（2012）43图二、用户查找并添加结论作为 [ H1 [ H2 H3]] ; auto;恢复 H;c l e a r H;n r o l l AllDefinition ;我不知道端一旦应用了这种策略，几何对象定义就被表1第二列中相应的谓词所取代。一些谓词，如l1≠l2，A/ = B。. .可以被认为是非简并的物体存在的条件。对于几何对象的许多定义，我们在假设中隐式地添加了非退化条件。这些条件对于推理非常重要，有时解决退化情况下的问题比解决原始问题更复杂同一个图，不同的构造方法，其非退化条件也不同4.2.1搜索和应用规则在这里，我们提出了一个反向链接的几何推理方法。这种方法从结论发展到假设，即我们需要证明GeometricElements，Hyp1. Hypn→目标。我们在一个规则集中搜索，以找到以下形式的规则：Gn→进球。问题演变为证明子目标G1，.， G n. 重复该过程，每个子目标，直到子目标在假设中或者是公理。在我们的界面中搜索适用的规则是使用搜索命令实现的。它足够强大，可以在数据库中找到导致模式给定目标的所有规则。从界面的证明窗口，用户可以搜索当前目标的所有适用规则。将显示适用规则的列表，允许用户选择适当的规则。在给出这个规则的参数值之后，这些参数通常是点、线。. . ，用户可以更新规则语句T.M. 范，Y。Bertot/Electronic Notes in Theoretical Computer Science 285（2012）4349图3.第三章。适用规则显示在底部，用户选择值以应用规则对于给定的值，系统通过验证其假设来检查正确性。回到我们的例子4.1，为了证明GF可达，我们需要找到结论形式为2行的规则。Search命令的一个变体被发送到ModuleName中的CoqSearchPattern（搜索模式）有了一个适用规则的列表（图3的上图），我们可以选择以下规则来应用。引理isosceles perp：AB C M：Point，B = C→ A = M→ AB = AC→ M=中点（B，C）→AM/ BC。使用四个点G，D，E和F分别作为其参数的值，我们有这个规则的一个实例（图3的下图）D/ = E→ G/ = F→ GD = GE→ F =中点（D，E）→GF→ DE。通过构造F，我们有F = MidPoint（D，E），因此应用此规则是合理的，它通过命令apply isosceles perp with（A：=G）（B：=D）（C：=E）（M：=F）执行。现在，我们必须证明GD = GE，而不是证明GF≠ DE。4.2.2添加新属性一般情况下，我们不能只使用反向推理来解决问题，另一种方法是使用正向推理。这个过程的目的是通过应用给定的规则从假设中生成新的属性这些属性在该过程的后续步骤中用作假设。 当过程可以生成目标时，它就结束了。 如果我们需要证明，几何元素，Hyp1，... Hypn→目标。在规则的基础上，我们有几何元素，Hj1，…hjm→目标j，{H j1，. H，j，m}是{Hyp1，...，Hyp n}，因此我们可以添加G j作为假设50T.M. 范，Y。Bertot/Electronic Notes in Theoretical Computer Science 285（2012）43的定理。我们的系统提供了一种前向链接的变体，允许用户在证明定理的同时添加新的属性。如果一个属性被证明，它就被用作一个假设。在我们的例子中，为了证明GD =GE，用户试图证明GD = GC和GE = GC。首先，用户在图中选择GD和GC两个段，右击用户可以找到它们的相等关系。系统要求用户将此公式添加到当前证明中。为了证明GD = GC，我们将使用以下规则：Lemma rightTriangle midPoint：ABCM：Point，A/ = B→ A = C→ line（A，B）中线（A，C）→M =中点（B，C）→MA = MB<$ MA = MC。通过我们例子中的4个点D、B、C和G的配置，我们有：A/ = B→ A = C→线（A，B）→线（A，C）→M =中点（B，C）→MA=MB→ MA = MC。第二种情况GE = GC也是如此。这就需要证明线（B，D）等于线（C，D），线（C，E）等于线（B，E）。他们被证明由于点D，E的建设和使用自动战术，我们将在稍后介绍4.2.3绘制辅助线有时，用户需要添加线，射线，段。. . 在他们的证明过程中。确保这些物体的存在是非常重要的在定理证明阶段，每个创建的对象只在某些条件下存在因此，当用户创建一个新对象时，他们需要在使用这个对象之前验证它的条件当用户创建2条线l1和l2的交点M时，以下命令被发送到Coq。l e tH：=F R E S H“isIntersectionPoint“I na s s e r t（H：e x i s t s M，M = I intersectionPoint l 1 l 2 ;apply e x i s t s\ intersection Point.Coq要求证明l1≠l2以保证M的存在性。一旦验证了该条件，点M将显示在绘图窗口中，并且将命令destruct H as [M，H]自动发送到Coq以假设M = IntersectionPoint（l1，l2））。4.2.4自动战术在Coq的支持下证明几何给出了高水平的置信度，每个推理步骤都得到了验证。但是，这也使证明过程复杂化。用户不仅决定应用哪条规则，而且还要证明许多小目标，这导致繁琐的证明，不适合教学设置。因此，为了避免在证明细节上压倒用户，我们试图提供自动解决这些问题的策略例如，我们提出了一种解决直线和直线上的点问题的策略在我们的例子中，我们必须证明直线（B，D）是直线（C，D），而我们有c =直线（A，C），d =平行直线（B，c），D =交点（c，d）。这个证明在T.M. 范，Y。Bertot/Electronic Notes in Theoretical Computer Science 285（2012）4351图四、用户可以在弹出菜单中使用自动战术Coq很详细。由c = line（A，C）我们有C∈ c。从D = IntersectionPoint（c，d）我们有D∈ c。所以我们有line（C，D）= c。我们也有line（B，D）= d。从假设d =cylinderLine（B，c）我们有d c，我们得到line（B，D）cylinderline（C，D）。这种复杂性来自Coq中线条的区别。例如，如果我们有一条直线l通过点M N P，我们很容易得到line（M，N）= line（N，P）=线（M，P）= 1。但这些线路不能自动地由系统相互替换。我们提供了以下策略来解决这个问题，通过发现点和线的所有关系，并将线（M，N）的所有实例替换为线l，如果在假设中发现M∈ l和N∈Ltac r e p l a c e auto Lines：=展开所有定义;匹配与...相处融洽|− context[ l i n e ？M？N]=>匹配戈阿勒与|H1：l iesOnLine M？L|−=>match 戈阿勒与|−= > try（r e p l a c e（l i n e（M，N））with l in N; auto）; r e p l a c e A l l L i n e N | −=>try ( r e p l a c e ( l i n e (M,N) ) with l in ∗ ; auto ) ;replaceAllLineInstances结束结束端对于每个特定目标，弹出菜单中提供了相应的策略（图4）。5执行52T.M. 范，Y。Bertot/Electronic Notes in Theoretical Computer Science 285（2012）43Geogebra是用Java实现的，它的架构清晰，并组织在单独的层和模块中。在上一个版本（v3.3.69）中，Geogebra的每个视图（如T.M. 范，Y。Bertot/Electronic Notes in Theoretical Computer Science 285（2012）4353图五.系统架构。绘图板、代数视图、CAS视图、电子表格视图）是通过扩展Java的JPanel类和实现View接口来独立实现的。因此，提供了一些功能，允许用户显示或隐藏这些视图，拖动以修改其位置，并在外部窗口中打开它们。公共i n t e r f a c e View{公共虚空添加（GeoElementgeo）;public void update（GeoElement geo）; publicvoid update（GeoElement geo）;. . .}由于控制器模块，这些视图在同步模式下工作这通过调用每个视图接口中的相应函数，将我们将Pcoq集成到Geogebra中，尊重这一架构（图5）。Pcoq是作为Geogebra的视图实现的。一旦它收到通知，就会产生相应的命令并发送给Coq。如前所述，通信信息是树格式的，因此需要一个模块来从结构中生成树格式命令以下代码行是在定理陈述阶段添加中点的示例：P R I V A TE树[ ]命令中点（GeoElementgeo）{//t-h i s 功能 I s 到 产生 命令 福或 一int [ ] nums = nums;AlgoElement parentAlgo = geo . getParentAlgorithm（）;GeoElement point1 = parent Algo . getInput（）[ 0 ] ; GeoElementpoint2 = parent Algo . int [ 1 ];内容 = 新Tree [ 2 ];联系我们[ 0 ]= TreeFormat . addVar（geo . getLabel（），TreeFormat . 点 ）的情况下;[ 1 ]第一届全国政协委员=TreeFormat . addHypothesis（“Hyp 中点54T.M. 范，Y。Bertot/Electronic Notes in Theoretical Computer Science 285（2012）43TreeFormat . a s s i g n Va r i a b l e（geo . getLabel（），TreeFormat .函数（TreeFormat . MidPointAB，第1点。get Label（），第2点。getLabel（）;return contents ;}在我们的实现中，我们继续了在Pcoq中已经讨论过的“通过指向证明”的概念它允许用户使用鼠标在证明助手的用户界面中精确地引导证明过程，即，指向目标或假设的子表达式的姿势足以为系统合成适当的命令。虽然Pcoq中的指向证明依赖于分析公式和理解逻辑符号的含义，但我们系统中的这一概念是通过公式的几何意义来实现的对于每个推理步骤，通过找出用户选择的子目标、假设的意义，系统可以在弹出菜单中提供适当的策略来指导用户解决问题。例如，我们确定所选目标的格式是否为（=行），（=氨氯地平）或（= parallelLine），在这种情况下，系统提供了替换自动线策略来解决它。6相关工作DGS越来越多地用于教育。 许多作品都被表演过 以提供DGS和GTP的组合。其中一些使用自动方法，允许用户证明几何定理。我们将在这里引用几个可以生成可读证明的系统。带有网络接口的Geothms[16]使用基于面积法的GCLC证明器。在几何定理知识库的支持下，用户可以存储定理陈述及其证明。MMP/Geometer[10]和GeoExpert[9]是实现Wu方法、面积方法、全角度方法（GeoExpert）以及特别是演绎数据库方法[ 7 ]的强大系统最后一种方法依赖于一组基本规则，并允许找出传统的证明。GeoExpert允许用户直观地了解生成证明的每个步骤Geometry Explorer[17]也实现了全角度方法。然而，它可以自动生成新的图形证明相应的推理所使用的GTP。这是一个很好的证明。Geoproof[15]与我们的系统非常接近。Geoproof中的推理由Coq执行，并基于该证明助手中面积方法的形式化[14]。由于Geoproof也使用了Coq，所以我们在陈述阶段会有一些类似的观点。主要的挑战在于定理证明阶段和系统连接到Coq的方式Geoproof只允许用户构造定理语句，将它们发送到CoqIDE，并通过应用面积方法来检查这一事实。它不允许用户逐步构建自己的证明，也不提供DGS和Coq之间的交互。T.M. 范，Y。Bertot/Electronic Notes in Theoretical Computer Science 285（2012）4355另一个将DGS与Coq相结合的工具是GeoView[2]，但该工具的工作方向相反。它从Coq中的定理语句生成DGS中的图，即GeoPlan。7结论和今后的工作在本文中，我们提出了我们的接口，允许用户交互式地构建传统的几何证明。给出了中学水平的推理方法，如向前法、向后法、画辅助线等。推理步骤由证明助手验证，因此保证了正确性。在动态几何软件中集成证明助手为几何学习提供了一种新的途径。它允许用户在解决几何问题时额外地具有逻辑视图。用户知道他们有什么假设，他们必须证明什么，他们可以应用哪些规则。. .通过这种方式，他们可以做出正确的决定，并彻底理解推理步骤。一些功能需要改进，以使用户能够轻松使用我们的工具。从规则语句动态构造图就是一个例子.使用规则的构造然后用户可以拖放这些对象来应用此规则。第二个问题是我们如何组织和管理适用的规则集和策略集，同时适应用户级别。引用[1] Amerkad，A.和Y. Bertot和L. Pottier和L. Rideau：2001，Mathematics and Proof Presentation inPcoq. 与IJCAR相关的研讨会证明转换和演示及证明复杂性[2] Bertot，Y.和F.Guilhot和L.Pottier：2004，Visualizing Geometrical Statements with GeoView.理论计算机科学电子笔记103：49-65[3] Bertot，Y. 和G. Khan和L. 历史：1994年，由波因特公司生产。计算机软件的理论方面[4] 周，S.-C.：1988年，介绍吴Journal of Automated Reasoning自动推理杂志4：237-267[5] 周，S.-C. 和X。-S. Gao和J. -Zhang：1994，Machine Proofs in Geography：Automated Productionof Readable Proofs for Geography Theorms。世界科学[6] 周，S.- C.和X。- S. Gao和J. - Zhang：1996，自动生成具有几何不变量的可读证明。全角度定理证明。自动推理杂志17：349-370[7] 周，S.- C.和X。- S. Gao和J. - Zhang：1996，A Deductive Database Approach to Automated GeometricTheorem Providing and Discovering. Journal of Automated Reasoning自动推理杂志25：219-246[8] Coq开发团队，Coq证明辅助参考手册。http://coq.inria.fr/refman/[9] 高，X。-史：2000年，几何专家，软件包。http://www.mmrc.iss.ac.cn/www.example.com~xgao/gex.html[10] 高，X。-S. 和Q.Lin：2002，MMP/Geometer-一个用于自动几何推理的软件包。自动演绎几何学会议录[11] Geogebra开发团队，GeoGebra简介。http://www.geogebra.org/book/intro-en/[12] Guilhot，F.：2005年，《C oq和可视化的一门课程》，为我们提供了一个机会。Technique et ScienceInformatiques 24：1113-113856T.M. 范，Y。Bertot/Electronic Notes in Theoretical Computer Science 285（2012）43[13] Kapur，D.：1986年，用Gr？obner基解决几何问题。JournalofSymBolicComputation 2：399-408[14] Narboux，J.：2004年，Coq中几何的决策程序。高阶逻辑定理证明会议录，LNCS 3223[15] Narboux，J.：2007年，一个用于几何形式证明的图形用户界面。Journal of Automated Reasoning自动推理杂志39：161-180[16] 阿雷雷斯马山口 和P. Jan izuc i'c：2007，G eoThms-aWebSystemforEuclid eanConstructiveGeometry.理论计算机科学中的电子笔记174：35-48[17] 威尔逊，S。和Jacques D. Fleuriot：2005，Combining Dynamic Geometry，Automated GeometryTheorem Proving And Diagrammatic Proofs. 欧洲软件理论与实践联合会议（ETAPS）论文集定理证明器用户界面卫星讲习班（CNOP）