理论计算机科学电子笔记103（2004）49-65www.elsevier.com/locate/entcs用GeoView可视化几何报表Yves Bertot伊夫·贝尔托1，2Lemme团队INRIASophia Antipolis，法国Fr'ed'eriqueGuilhot3Lemme团队INRIASophia Antipolis，法国LoıcPottier4Lemme团队INRIASophia Antipolis，法国摘要我们描述了一个工具，它结合了一个通用的定理证明器和一个开放的货架接口动态几何绘图，以提高人机交互涉及几何证明。使用我们的工具，我们可以编辑几何定理的语句，使用定理证明器构造和验证它们的证明，并使用绘图工具可视化语句。关键部分是一个算法，它计算从定理的形式陈述中得出一个结构所需的数据。本文包括一些例子，从我们的组合工具，称为GeoView的输出。保留字：定理证明，几何，动态几何绘图。第一，从技术上讲，这是GeooplanJ为他提供的一个全面的解决方案。2电子邮件：Yves. sophia.inria.fr3电子邮件：Frederique. sophia.inria.fr4电子邮件：Loic. sophia.inria.fr1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.09.01350Y. Bertot et al. / Electronic Notes in Theoretical Computer Science 103（2004）49-1介绍基于高阶逻辑的通用定理证明器通常提供交互式证明的可能性。由于交互方面，用户需要发展逻辑和推理能力。人们很自然地认为，这种要求使得这类定理证明器成为帮助学生学习数学的好工具。为了研究这种使用的交互式定理证明器在域的geome-尝试，我们已经开发了一个图书馆对应的课程，在法国高中系统。这些课程包括二维欧几里德几何，三角形，圆，基本变换，如平移，旋转，同构和三维几何与平行，inci- dence和直线和平面之间的正交问题。我们选择避开解析几何，因为在解析几何中，推理不如计算重要所有这些工作都是使用图形用户界面进行的，这使得协调形式语言（来自定理证明器）和通常的数学符号（更适合于人类之间的交流，如教师和学生）的要求成为可能。在这种情况下，人们很快就清楚地认识到，“一幅好的图画胜过冗长的解释”。我们设计了一个图形界面的扩展，这样绘图会自动与数学公式相关联，以显示这些语句的含义。我们的主要设计决策是重用现有的绘图工具。我们集中在法国数学教师已经可用的工具上，特别是GeoplanJ [9]，主要是因为它可以通过GNU GPL许可证获得。我们的结果组合工具称为GeoView [12]。本文的组织如下：在第二部分中，我们描述了证明开发工具，我们使用的几何事实，我们已经在这个环境中开发的理论;在第三部分中，我们总结了独立的绘图工具，我们集成在证明环境的功能。第四部分描述了我们贡献的关键：一个将逻辑语句转换为图形构造序列的排序算法。第五节以一系列重要实例说明我们的结果。第六部分对相关工作进行了研究，并提出了几点结论。2Pcoq和几何库Pcoq是我们开发的证明开发环境[4]，作为Coq系统的前端[18]。Y. Bertot et al. / Electronic Notes in Theoretical Computer Science 103（2004）49-512.1Pcoq证明环境Pcoq [1]是通用定理证明器Coq的用户界面，它将所有公式和命令作为树状结构（也称为抽象语法树）而不是纯文本进行操作。该特性使得容易提供在不给出结构的环境中难以获得的设施。例如，Pcoq可以很容易地将特殊的数学符号附加到某些函数上，从而使向量、平行和垂直谓词以及角度的特殊符号成为可能。我们的数学符号的例子将自然出现在下面的图表中。对命令结构的简单访问也使得将自然语言中的句子附加到几何语句中变得容易。在图1中，我们可以看到一个具有Coq默认语法的语句，以及与Pcoq相同的语句。引理isosceles_median_bisector：（A，B，C，I：PO）~（A==I）->~（B == C）->（I==（中点BC））->（等腰A B C）->（cons_AV（vec A B）（vec A I））==（cons_AV（vec A I）（vec AC））。Fig. 1. Pcoq中自然语言的符号和句子示例这种自然语言表示主要用于输出，它不能用于输入文本（这将需要自然语言解析），但向用户建议句子模板用于鼠标引导的输入。正如在以前的作品中发表的[1，15]，自然语言也可以用来为Coq构建和验证的证明提供可读的形式。结合逐点证明，所有这些都为数学教师和学生提供了一个良好的支持证明环境。使用树结构在GeoView中也起着重要作用。对应于定理或猜想陈述的树可以很容易地被分析以生成图形文本，这些文本被传输到GeoplanJ（在第3节中描述）用于绘制和显示。还有一些工作要把状态与适当的图形结构联系起来，这项工作在第4节中描述52Y. Bertot et al. / Electronic Notes in Theoretical Computer Science 103（2004）49-2.2我们的Coq几何库我们使用Pcoq开发了一个几何定理库，该库包含了法国高中教授的课程。这个图书馆是基于一个大集合的公理，这不是选择是最小的，而是要对应的细节，学生应该理解和掌握的水平。学生们不应该知道代数概念，如向量空间，a-rusne空间，或度量，但尽管如此，他们应该熟悉向量运算，如加法，标量乘法，标量积等。重心计算的一般概念不能系统地使用，但重心的概念是可用的。我们的公理化与Marcel Berger在他的著作[ 3 ]中对重心和泛空间的描述有很大的关系在我们的库中，大多数运算不是由定义给出的，而是由假设某个函数存在并满足一两个公理给出的。我们在这里只列举我们可以用二维图表示的平面几何的不同基本概念：• 向量、对齐、重心、中点、质心、平行度，• 正交性，正交中心，正交投影，• 欧几里得距离，等腰三角形，垂直平分线，圆，与圆相切的线，相切圆，• 同构、平移、反射、旋转、这些变换的直接相似性和合成、反转。• 复数我们证明了平面几何中的一些经典定理，用的方法与高中课程中的方法相同。其中，我们可以举出：泰勒斯、墨涅拉俄斯、塞瓦、笛沙格、毕达哥拉斯、西姆森在这个库中，也有关于三角学和三维几何的章节，我们还没有连接到一个绘图工具。3地理规划GeoplanJ [9]是CNAM开发的动态几何图形绘制工具在本节中，我们描述其正常行为。Y. Bertot et al. / Electronic Notes in Theoretical Computer Science 103（2004）49-533.1在GeoplanJ中操作的对象用户在配备了预定义但不可见的坐标系的平面上创建数学对象。对象可以属于多个类。 有些是可画的：点、直线或曲线，而有些则是不可画的：实数、向量、同位性、平移等。有些对象是自由的，如任意点，而另一些则是有界的，如定义为穿过其他点的线、属于线的点、中点等。所有对象都有一个描述其在实际图形中位置的值。可变对象可以作为用户交互的结果而移动，通常是当用户通过用鼠标指向并通过拖动来移动空闲点时。因此，我们可以为同一个图形获得几个图形，对应于变量对象的不同值。在图2中，我们显示了与图2相对应的几幅图，其中A，B和C是自由点，D是通过C并平行于线（AB）的线上的自由点，I和J分别是线段[AB]和[CD]的中点，并绘制了三条线（AC），（BD）和（IJ）图二. 同一图形变量对象和自由对象之间的区别是有意义的：有些对象可能同时是变量和绑定的。例如，一个点可能被约束在一条直线上，但仍然可以改变它在直线上的位置，如图2中的D地理平面图是对点的描述的集合，包括将它们绑定在一起的约束。每个图形都可以保存为一个文本，其中所有对象都被枚举。它还可以包含额外的信息，如颜色，线条样式，名称。可以让GeoplanJ简单地通过给出描述它的文本来绘制一个图形。54Y. Bertot et al. / Electronic Notes in Theoretical Computer Science 103（2004）49-3.2集成GeoplanJ软件GeoplanJ 是 GeoplanW [11] 软 件 的 部 分 Java 端 口 ， 它 最 初 旨 在 用 作applet，但由于它是在非常自由的许可下作为自由软件提供的，因此我们能够使用它并为我们的目的修改它我们的证明开发工具的主要部分也是用Java语言编程的，因此在我们的软件中包含GeoplanJ是一件容易的事情。GeoplanJ使用与GeoplanW完全相同的文本格式来描述数字，因此我们实验中生成的数字可以使用两个软件重复使用和修改。4GeoView一些出现在几何陈述中的谓词，如共线、共循环和等腰是多方向的：当这些谓词接受n+ 1个自变量时，给定其中的n个，可以确定对最后一个的约束。然而，需要做一些工作来决定这些谓词用于构建与语句相关联的图形的顺序。 这项工作是由我们在本节中提出的算法完成的4.1数据分析对应于作为输入给出的定理陈述的数据在类型为H 1 →.的树中变换。→Hn→C其中Hi可以解释为定理的前提，C可以解释为定理的结论。然后，我们区分约束和非约束几何约束：例如，约束（共线ABC）是约束，但（非（共线ABC））是非约束：一般来说，平面上的任何三个点都是方便的。结论中出现的约束对于构建来说是多余的：它们是不具约束力的。我们列出了所有的约束条件和其中出现的点。从这个列表中，4.2中详细描述的算法确定了具有GeoplanJ语法的图形文本。4.2从几何约束集构造点集给定实平面上的一组有限的点，以及这些点上的一组有限的几何约束，我们描述了一个简单的算法，该算法可以产生这些点的构造，适合于绘制满足几何约束的这些点的图像。Y. Bertot et al. / Electronic Notes in Theoretical Computer Science 103（2004）49-55几何约束一个几何约束可以表述为一组关于点坐标的多项式等式：说点A、B、C共线 等 价 于 一 个 多 项 式 等 式 ： （ xC−xA ） （ yB−yA ） = （ yC−yA ）（xB−xA）。几何约束被写为（CP1. P n），其中C是约束而P1P n是点。我们将主要限制自己的约束条件，这样，对于一些选择n-1点之间的P1. P n，我们可以通过简单的几何构造来构造剩余的点.例如，对于约束（共线ABC），我们可以自由选择两个点，第三个点被约束在由其他两个点定义的直线上对于约束C，我们关联一个列表T（C），该列表描述了取决于点在约束中的位置的点的自由度如果点Pi完全由其他点确定，则约束在位置i具有类型2（即，确定点的两个坐标）。如果Pi可以在曲线上变化（例如圆或直线），则约束为在位置i的类型1。 如果存在点Pj（j = i）的配置，使得约束（CP1.. Pn）不能满足，那么我们就不能选择自由点Pj（j位置岛i) 我们说约束的类型为0，例如，对于约束（反射ABMN），其意味着N是通过相对于线（AB）的反射的M的像点，点N完全由其他三个点A、B和M的位置确定，我们说约束在位置4中是类型2。但是为了构建B，我们不能自由地选择三个点M，N和A，因为A必须位于线段[MN]的垂直平分线上，我们说位置2的约束类型为0。下面是两个例子：(i) 对于约束（共线ABC），这意味着A，B和C是共线的，我们有T（共线）=（1， 1， 1）。(ii) 对于约束（反射ABMN），这意味着N是M通过关于线（AB）的反射的像点，我们有T（反射）=（0， 0， 2， 2）。56Y. Bertot et al. / Electronic Notes in Theoretical Computer Science 103（2004）49-Σ构造点要使用其他点的约束来构建一个点，我们需要考虑它在约束中的位置，并且我们可能必须构建中间对象。例 如 ， 在 约 束 （ 等 腰 ABC ） 中 ， 这 意 味 着AB=AC，为了构建点A，我们构建[BC]的垂直平分线，但是为了构建点B，我们构建半径为[AC]的圆心A如果一个点出现在两个约束中类型1的位置，我们建立两个几何对象（两条直线，两个圆或一条直线和一个圆）的交点。从限制到建设我们现在可以描述如何建立一组点P1，...，Pm满足一组约束（C1Q11. Q1r1），. ，（Cn Q n1. Q nrn），其中Qij，Q ij∈ {P1，. ，Pm}。我们定义了n行m列的策略矩阵。对于每个约束，我们将链接点定义为使用该约束从其他点构建的点。矩阵M的每个条目Mij描述了如何相对于约束Ci使用或产生点Pj。我们需要找到一个矩阵来验证条件：（i）ij，Mij∈ {−1， 0， 1， 2}，(ii) ij，Mij=−1惠Pj不出现在约束Ci中，(iii) ij，Mij>0(iv) M的每一行都恰好有一个严格正项，(v) i，i_sup（0，M_ij） ≤2，(vi) 关于点P1，...，P m定义为当M_b= 0且M_b> 0时，其过渡闭合度是对称的.条件（iv）意味着每个约束将建立一个新的点（如果其位置是类型1，则可能不完全确定条件（v）表示一个点由一个或两个约束建立，如果它由两个约束建立，则它是两个曲线对象的交点Y. Bertot et al. / Electronic Notes in Theoretical Computer Science 103（2004）49-57条件（vi）意味着构造不会循环：我们不会使用一个已构建的点来构建一个旧的点。找到这样一个矩阵的算法现在很容易描述。 我们首先建立一个矩阵M，验证条件（i），（ii），（iii）和（iv），其中每一行的正项都是最左边的，这很容易。我们列举了所有的矩阵验证条件（i），（ii），（iii）和（iv），简单地通过字典顺序移动每一行的积极的条目到右边。只要矩阵满足条件（v）和（vi），我们就停下来，这两个条件很容易检验。否则，我们就失败了。如果这个算法没有失败，我们可以直接使用矩阵M来获得点的有效构造：关系的极小点p通道上的自由点是p阶（其中p阶是p阶）。从这个点集，称为S0，具有约束，我们可以建立一个新的点集S1（这是在（{P1， . . ，Pn} -S0），以及son。 对于每个点，使用约束生成GeoplanJ命令。让我们以以下几点和限制为例。C1：（共线A B H）C2：（orthoH C A B），即直线（HC）和（AB）垂直。C3：（圆A B C），即C在直径为[AB]的圆上。我们有以下类型的职位：T（共线）=（1， 1， 1）T（ortho）=（1， 1， 1， 1）T（圆）=（1，1，1）设P1，. ，Pn= A，B，C，H.验证条件（i）、（ii）、（iii）和（iv）的初始矩阵为：M一 B CH共线1 0 −1 0Ortho1 0 00圈1 0 0−1它不验证条件（v）：列A由三个约束链接。按照字典顺序，下一个矩阵验证条件（i），（ii），（iii）58Y. Bertot et al. / Electronic Notes in Theoretical Computer Science 103（2004）49-和（iv）是：M一 B CH共线1 0 −1 0Ortho1 0 00圈0 1 0−1它验证了条件（v），但不是条件（vi）：我们有BAB继续，我们得到验证条件（v）和（vi）的第一个矩阵M一 B CH共线1 0 −1 0Ortho0 0 10圈0 0 1−1我们有BA，H A，AC。然后，构造为(i) 在平面上取B和H(ii) 取A为直线（BH）上的自由点。(iii) 设C为与（AB）正交且包含H的直线与直径为[AB]的圆的交点。一般配置、限制和改进关于自由点（在平面上、在直线上或在圆上）的整个讨论仅一般地成立，即：在一组特定情况之外（例如，平面中的三个自由点可以共线等）。但是这个集合在Rn中是有限测度的，所以当随机选择自由点时，我们有很高的概率摆脱这些退化的情况。这种方法是不完整的。从一组可解的几何约束出发，它可能无法给出一个构造。原因是我们研究的是点上的非线性约束：这种约束不是在点上而是在坐标上，或者在更复杂的结构上（例如射影点的行列式）定义了一个很好的自由度。该方法虽然不完全，但具有简单、快速的优点，并且在一般使用中很少失败。Y. Bertot et al. / Electronic Notes in Theoretical Computer Science 103（2004）49-595几个说明性的例子在分析矩阵之后，一个图形文本被传输到GeoplanJ，这样在生成的图形中，自由点显示为绿色，结论显示为红色。用户实际上可以移动自由点，并且图形相应地演变5.1辛生我们证明了Coq Simson这个定理指出：给定一个三角形，M是平面上的一点，从M到三角形边的三个直角尺共线当且仅当M在三角形的外接圆上图三. Simson在图3中，我们显示了Pcoq中出现的这个定理陈述以及GeoView生成的相应图。在这个例子中，定理的结论是两个命题的等价。对于GeoView，我们将第一个视为前提，第二个视为结论。60Y. Bertot et al. / Electronic Notes in Theoretical Computer Science 103（2004）49-5.2九点圆定理我们在Coq证明了九点圆定理，也被称为欧拉给定一个三角形，这个圆通过三条边的中点，每条边的垂线的脚通过相对的点，也通过连接顶点和正交中心的线段的中点我们还证明了这个圆的中心是连接三角形的外心O和正交心H的线段的中点，三角形的质心G位于线（OH）上，这被称为欧拉在图4中，我们显示了Pcoq中出现的这个定理陈述，以及GeoView生成的相应图，其中A，B和C是唯一的自由点。5.3析取出现在定理前提中的析取意味着实际上必须考虑几个数字，每个数字对应一个析取。出现在定理结论中的析取对应于这样一个事实，即同一个图形可能出现几个配置。这在定理中得到了说明，该定理指出：给定梯形ABCD，I和J分别是线段[AB]和[CD]的中点，三条线（AC）、（BD）和（IJ）相交或平行。对应于该定理的图形如图2所示。5.4表示实数在矢量表达式或几何变换（如旋转、相似性或反转）中出现的实数显示为固定直线上的点，显示在图形的顶部，如图6所示。用鼠标移动该点可以改变实数的值，其他几何对象依赖于这个实数移动。5.5潜在量化正如我们已经说过的，在声明的结论中出现的约束通常是不具约束力的。如果结论是存在性量化，那么这引入了约束条件，即使它们出现在结论中。通过向量−A−→AJ的转换的组合给出了一个示例以及中心I和比率k的非平凡同素性。该定理指出，Y. Bertot et al. / Electronic Notes in Theoretical Computer Science 103（2004）49-61见图4。 九点圆定理：Pcoq中的语句和GeoView62Y. Bertot et al. / Electronic Notes in Theoretical Computer Science 103（2004）49-存在一个点J，它与点I，A和AJ有界，k的homothety。定理陈述出现在Pcoq中，如图5所示。图五. 翻译的合成与同位：Pcoq相应的图形可以绘制如下。 在动态图形中，每当I、k、A和AJ移动时，J就移动，但当B移动时，J不移动。点J独立于B，这可以通过定理陈述中的泛量子数或存在量子数的嵌套来表达。图六、一个翻译和一个同构的组合：由GeoView生成的图形5.6表示复数复数可以在高斯平面中表示。对于一个给定的复数形式x+iy，我们将表示点与坐标（x，y）相关联。在图7中，我们展示了一个引理的陈述，该引理给出了从复数的极坐标形式计算复数的实值和虚模数r（距离）和z的参数a（弧度数）是实数，因此在图形顶部显示为直线上的点。您可以通过更改r和a的值来移动表示z的图像点。Y. Bertot et al. / Electronic Notes in Theoretical Computer Science 103（2004）49-63见图7。 转换公式：Pcoq中的语句和GeoView6总结发言6.1相关工作我们的工作是在两个领域之间的边界：第一个是关于交互式绘图，而第二个是关于推理工具。用于几何构造的绘图工具比比皆是。许多可以在Web浏览器中使用的Java小程序可以通过在万维网上搜索轻松找到。例如，我们可以引用GEONExT [10]和D.E. [13]我们可以很容易地找到和测试。在我们的工作中，我们专注于数学教师已经使用的工具，如Cabri-Geometre [19] ， EUKLID DynaGeo [8] （ 我 们 还 没 有 使 用 ） ， 以 及GeoplanW和GeospaceW [11]。几何推理工具也可以分为两类。第一类使用分析方法将几何问题简化为代数问题，并使用有效的代数工具（如grobnerba ss）来解决后者。第二类依赖于证明者，通常是一阶证明者，从描述几何的公理集合中推导事实。在第一类中，我们可以引用周尚卿的工作[5]，在第二类中，可以引用多米尼克·皮的工作[17]或尼古拉斯·巴拉什管理的莱布尼茨实验室[2]。我们的工作更接近于第二类，特别是因为在所有这些实验中，工具是一种教学辅助工具的观点占主导地位。在64Y. Bertot et al. / Electronic Notes in Theoretical Computer Science 103（2004）49-特别是，Baghera [20]还提供了显示与练习相关的绘图的方法，但它负责从教师或学生的角度组织教室或书包这项工作也涉及到用通用定理证明器形式化几何的方法。我们可以引用文献来形式化希尔伯特6.2结论读者应该清楚，我们在本文中描述的设计很容易适应其他证明或绘图工具。几何库本身应该很容易用任何其他证明工具来描述，甚至公理化本身也可以改变。实验只需要映射的基本概念从几何图书馆的基本概念的绘图工具：点，路线，共循环约束等，例如，Cabri-Geometre是在法国学校系统中使用的最流行的工具之一，它似乎很容易适应我们的工作，这个绘图工具。本实验中提出的交互模型仅使用绘图工具作为输出设备：公式取自书面形式并转换为图形描述。考虑反向交互方案将是有趣的，其中一个图形将通过与绘图工具交互使用鼠标来描述在这个扩展中，绘图工具可以用来提高证明环境的输入能力。反过来也是相关的，逻辑语句是绘图的规范，可以用作绘图工具的新输入语言，比当前的文本输入格式或鼠标交互更简洁。另一个观点是使这项工作适应三维几何。在二维屏幕上表示三维对象会带来困难。三维空间中的平面很难以高效的方式渲染。通常的技巧是用一个包含在平面中的线来表示平面，但是这样两个相交的平面不能保证在任何图形中都显示相交。相反地，当图像被呈现在屏幕上时，不相交的两条直线可能看起来相交。引用[1] A. Amerkad，Y. 贝尔托， L. 波蒂埃， 和L. 里多 数学 和证明 在Pcoq中的介绍。 在车间证明转换和演示和证明的复杂性Y. Bertot et al. / Electronic Notes in Theoretical Computer Science 103（2004）49-652001年6月在意大利锡耶纳举行的IJCAR 2001[2] N. Balache，http://www-didactique.imag.fr/。[3] M.伯杰《几何学I》，第一章“重心;宇宙空间”，第67-83页。Springer，1987年。[4] Y. Bertot和L.特里为定理证明器构建用户界面的通用方法符号计算杂志，第25卷，第161-194页[5] S. Chou，X. Gao和J. Zhang. 几何机器证明：几何问题可读证明的自动化生产。世界科学，1994年。[6] C. Dehlinger 和J.F.杜福形式化曲面分类的交换定理。在 TPHOLsLNCS 2410 ，SpringerVerlag，2002年。[7] C. Dehlinger，J.F. Dufourd，and P. Schreck.希尔伯特初等几何中的高阶直观形式化和证明。在几何中的自动演绎，第306- 324页[8] EUKLID DynaGeo，http://www.dynageo.de。[9] GeoplanJ，http://mapage.noos.fr/fkotecki/geoplanj.html。[10] GEONExT，http://geonext.uni-bayreuth.de。[11] GeoplanW，http://www2.cnam.fr/creem/geoplanw/geoplanw.htm的网站。[12] GeoView，http://www-sop.inria.fr/lemme/geoview/geoview.html。[13] D.E. 乔伊斯， http://aleph0.clarku.edu/djoyce/java/geometry/geometry.html。[14] L.I. Meikle 和J.D. 弗勒里奥正式确定 希尔伯特第 Isabelle/Isar的Grundlagen在TPHOLs[15] H. Naciri和L.里多使用MathML在自然语言中的形式数学证明：在阿拉伯语证明中的应用。MathML国际会议：Hickory Ridge会议中心，芝加哥，IL，美国，2002年6月28-30日[16] D. Pichardie和Y.贝尔托形式化凸壳算法。在TPHOLLNCS 2152，Springer Verlag，2001年。[17] D. 是的。EnvironnementsInteractifsd' App r ent is ssag e et D ′ e monst r a t i o n e n g ′ eo m ′etri ie. Habilitation`aDir ige r d esRech er ch es，Universit′eddeRennes1，2001.[18] Coq开发团队Coq Proof Assistant：参考手册：版本7.2。 技术报告RT-0255，INRIA，2002年2月[19] J. 文森特用卡布里几何探索二维空间2。维多利亚数学协会[20] C. Webber和S.讨厌通过联盟形成紧急诊断。在Garijo F.，编辑，第八届伊比利亚美洲人工情报会议（IBERAMIA 2002年），第755LNAI 2527，Springer Verlag。
我的内容管理
展开
