基于Web的几何探索框架——GeoThms的功能与接口解决方案

理论计算机科学电子笔记174（2007）35-48www.elsevier.com/locate/entcsGeoThms --欧氏构造几何Pedro Cristoresma佩德罗·马雷斯马1，2科英布拉大学数学系葡萄牙科英布拉PredragJanicic3，4贝尔格莱德大学数学系Studentski trg 16，11000贝尔格莱德，塞尔维亚黑山摘要GeoThms是一个基于Web的几何知识探索框架，集成了动态几何软件（DGS），自动定理证明器（ATP）以及几何构造，图形和证明的存储库。GeoThms用户可以轻松地使用/浏览现有的几何内容，内容. 在本文中，我们描述了GeoThms的功能，重点是系统所需的接口解决方案，旨在通过互联网支持学习和教学几何GeoThms是一个可公开我们相信，在所有用户的帮助下，它将成为几何学的重要互联网资源。关键词：网络接口证明系统，自动几何定理证明，动态几何软件。1引言我们的动机是建立和维护一个公共访问和广泛使用的互联网为基础的框架建设性几何。它应该用于几何教学和研究，但也作为一个主要的互联网知识库的几何插图。我们已经建立了一个系统，GeoThms，链接动态几何软件1这项工作得到POSC方案的部分支助。2电子邮件地址：pedro@mat.uc.pt3这项工作得到了塞尔维亚科学技术部144030号拨款的部分支持。此外，部分由POSC方案支持，由国际数学中心（CIM），在“研究配对”方案下，同时根据科英布拉集团招待计划访问科英布拉大学。4电子邮件：janicic@matf.bg.ac.yu1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.09.02036P. Quaresma，P. 《理论与计算科学》电子期刊174（2007）35(DGS)，自动定理证明器（ATP），和GeoDB，一个几何构造，数字和证明的数据库。GeoThms中目前使用的DGS是GCLC [7，12]和Eukleides [16，18]，这是两种广泛使用的动态几何包。使用的ATP，GCLCprover [13，17]，是基于面积法[4，6，15，17]，它产生人类可读的，合成的几何证明。GeoThms提供了一个Web工作台，将上述工具紧密集成到一个单一的构造几何框架中。Web界面是一个用PHP编写的服务器端解决方案，旨在使GeoThms用户能够轻松浏览几何问题列表，其陈述，插图和证明，并交互使用绘图和自动证明工具。GeoThms可在http://hilbert.mat.uc.pt/www.example.com有几个系统与GeoThms相关其中一些结合了DGS和自动定理证明器的功能，其中一些具有Web界面，其中一些提供几何定理的存储库我们不知道有任何系统，像GeoThms，提供完整的，基于Web的访问DGS，使用定理证明与人类可读的证明生成，并提供开放的几何结构和几何图形库第6节详细介绍了相关工作。文件概述。第2节介绍GeoThms组件;第3节介绍Web界面的结构;第4节介绍通信和表示问题;第5节通过一些示例介绍GeoThms。第六节讨论相关工作。第7节讨论了进一步的工作，第8节得出了最后的结论。2框架组件GeoThms是一个框架，它链接了动态几何软件、几何自动定理证明器和几何问题库，为所有这些工具提供了一个通用的Web界面（见图1）。在本节中，我们简要介绍了目前集成在GeoThms中的工具：GCLC和EukleidesGCLC5 [7，12]和Eukleides6 [16，18]是两个DGS。他们都使用说明性语言来指定几何结构。因此，在使用这些工具时，制作数学插图是基于“描述数字”而不是“绘制数字”。这些描述直接反映了数学对象的意义，并且易于数学家理解。这两种工具都有一个特定的需求和需求，在LATEX表格中，将使用这一点对应于几何结构。5 GCLC软件包可从www.matf.bg.ac.yu/janicic/gclc/免费获得。镜像版本可从EMIS（欧洲数学信息服务）www.emis.de/misc/index.html获得。有用于Windows和Linux的GCLC版本。6Eukleides可从http://www.eukleides.org获得，有多种语言版本。本文的第一作者负责Eukleides的葡萄牙语版本：EukleidesPT可从http://gentzen.mat.uc.pt/获得EukleidesPT/P. Quaresma，P. 《理论与计算科学》电子期刊174（2007）3537Web我nterfaceFig. 1. GeoThms框架GCLCproverGCLCprover是基于面积法的ATP [4，6，15]。它允许对在DGS内构造的对象进行形式演绎推理它证明了arehuman-reable（inLATEXanddXMLformats），并且对于每个证明步骤都有一个简单的判断。 GCLCprover与GCLC紧密集成，因此可以使用证明者对GCLC结构进行推理，而不需要改变和适应演绎过程，用户只需要添加他们想要证明的结论。在GCLC中进行的几何构造在内部转化为面积法的原始构造 ， 并 在 某 些 情 况 下 引入一 些 辅 助 点 。 我 们 已 经 开 发 了 一 个 工 具euktogclcprover，转换Eukleides文件转换为GCLCprover文件，允许将证明器与几何Eukleides中描述的结构GeoDB数据库geoDB保存几何构造、插图、插图和证明。图2显示了数据库的结构。数据库的主要实体是：几何结构的描述;定理，定理陈述，LATEXForm中的文字;profs，具有约束力的几何结构。几何构造以动态几何工具（如GCLC和Eukleides）的声明语言描述并存储在数据库中，一种通用的XML格式。图形由GCLC及Eukleides根据几何规格直接产生，并储存为JPEG文件及SVG文件。猜想是以一种扩展了几何构造描述的形式来描述和存储的.使用的规格（直接或通过贡献者表格（插入/更新数据）经常使用者交互模块存储库声明几何构造带猜想的几何作图报表图证明（证明人/抽屉/.）经常使用者报告（清单/技术报告）ATP（GCLCprover，.）DGS(GCLC，Eukleides，.）胶乳+辅助工具38P. Quaresma，P. 《理论与计算科学》电子期刊174（2007）35userIdbibrefId骨样骨样demIddrawerIdproverId作者作者证明者校准仪作者抽屉计算机证明图措施定理codeTmpProver代码Tmp比布雷夫斯用户图二. geoDB -权限关系图转换器）。 证明由GCLCprover生成，并存储为XML文件（由XML渲染，使用GeoConsproof.xsl指定的布局）和PDF文件（由LATEX渲染，使用gclcproof.sty指定的布局）。一个几何定理可以有不止一个图形和/或不止一个证明，由不同的工具和不同的用户制作。该数据库还具有以下辅助实体：bibrefs，书目参考，BIBTE X格式;抽屉式校准器，关于可用程序的信息;作者，关于作者的信息;用户，关于注册用户的信息;计算机，关于用作测试台的计算机的信息表codeTmp和codeTmpProver用于存储GeoThms交互部分的临时信息，在每次会话后删除。3Web界面的一般结构Web界面的结构有两个主要层次（参见图3）。所有Web用户都可以访问的入门级（见图4）包含一些有关GeoThms的基本信息，包括有关GCLCprover和面积方法的文档。还有一个进入GeoThms论坛的入口点。此级别提供注册选项，并允许访问系统的其他级别。普通用户可以访问第二层，在那里他们可以浏览数据库中的数据（以格式化或纯文本形式），并使用绘图/验证程序进行交互式工作。普通用户可以申请贡献者身份，他们也可以插入新数据，并可以更新以前插入数据库中的数据。还有一个管理级别，对用户不可见。它用于更改用户的状态和其他管理任务。P. Quaresma，P. 《理论与计算科学》电子期刊174（2007）3539GeoThms帮助入门级普通用户贡献者报告工作台形式2级名单：几何定理陈述数字证明所有的信息一起证明DrawersAuthorsBibRefs与绘图工具的交互插入/更新信息几何定理报表数字证明校准仪DrawersAuthorsBibRefs图三. GeoThms - Web界面4沟通和代表问题GeoThms是一个服务器端Web系统，集成了DGS和ATP工具。它不面向某些特定的浏览器和/或操作系统。作为一项网络服务，GeoThms强调：• 基于使用底层几何工具的几何规范语言的简单界面;• 低通信负担。为了实现这些目标，我们决定使用服务器端Apache/PHP/MySQL解决方案，以及HTML语言的标准功能来处理输入/输出。关于描述几何构造和几何图形的基本通信是基于底层几何工具的形式语言。尽管基于点击的结构描述有一些好的特点，我们见图4。 网站首页注册/登录40P. Quaresma，P. 《理论与计算科学》电子期刊174（2007）35我认为，在这种情况下，基于文字描述的沟通是一个更好的解决方案。例如，这种方法可以完全访问底层系统，不同的几何工具可以统一集成，强调几何构造是正式程序等。请注意，目前支持的两个DGSs工具（GCLC和Eukleides）也提供图形界面，因此用户可以在本地使用这些工具关于数据的内部表示，在GeoThms中，构造和推测的描述存储为GCLC代码，Eukleides代码或XML形式。有工具可以在这些格式之间进行转换，而XML格式作为交换格式具有中心地位当添加新的几何工具时，开发从其格式到XML的转换器将是足够的，反之亦然。这使得能够从任何格式转换到任何其他格式，从而使整个存储库可用于任何几何工具。数字以JPEG格式存储，但也以SVG格式存储。在GeoThms中，数据显示在：文本形式，具有以下选择：作为GCLC代码、作为Eukleides代码、作为呈现为HTML的XML（通过适当的XML）、作为以自然语言（英语）形式呈现的XML（通过适当的图形形式：有以下选择：JPEG图像，或SVG图像。参考文献以BIBTE X格式保存，可以获得一个BIBTE X文件，其中包含选定参考文献的列表。5GeoThms Tours在本节中，我们将通过一系列GeoThms Tours来描述GeoThms框架，GeoThms用户可以在与GeoThms的交互中使用一系列路径。5.1登录/注册在入门级（除了“帮助”部分）是“登录”部分，GeoThms用户可以登录，或新用户可以注册到GeoThms。 这是 一个标准的登记表，有强制性和可选的数据字段，并可选择是普通用户还是投稿人。如果一个普通用户想成为贡献者，他/她的请求将被发送给管理员，管理员有责任更改用户的状态。还有一个匿名帐户，用于快速初步使用GeoThms。只有注册用户才能进入第二层。普通用户可以从数据库中浏览数据，并以交互方式使用绘图/校对程序。贡献者还具有插入新数据和/或更新现有数据的权限P. Quaresma，P. 《理论与计算科学》电子期刊174（2007）35415.2浏览注册用户可以访问在这一部分中，用户可以浏览数据库中的数据、文件、定理和证明。对于这些组中的每一个，都显示了一个可用项的列表以及相关的详细信息（参见图6）。它也可以看到相关的信息证明人，绘图员，作者的程序和参考书目。图五. GeoThms见图6。 GeoThms5.3添加新数据贡献者可以访问“添加/更新”部分，在那里他们可以添加新数据和/或更新现有的结构，结构和证明。结构和图形由用户输入。只有由内置证明器生成的证明才能添加到数据库中。实体之间的关系迫使每个图形和/或证明必须与一个几何猜想相联系也就是说，贡献者42P. Quaresma，P. 《理论与计算科学》电子期刊174（2007）35见图7。 GeoThms必须首先添加一个几何猜想，只有在此之后，才能继续为该猜想添加一个图形和/或证明。一个贡献者可以添加一个几何猜想，它的陈述，相应的图形和证明，在一个单一的步骤或在不同的步骤。陈述必须首先出现，对于一个给定的猜想，可以添加不止一个图形和/或证明。贡献者还可以更新与图片、文件和证明相关的数据见图8。插入表格还可以插入/更新有关证明人、绘图人、作者和参考书目的信息。5.4协调作业在“交互式工作”部分，GeoThms向用户提供了以交互式方式使用DGS和ATP的可能性。GeoThms用户可以提交代码，要求对其进行评估，如果没有错误，可以查看结果图或P. Quaresma，P. 《理论与计算科学》电子期刊174（2007）3543证据如果出现语法、语义或演绎错误，则会显示错误消息，用户有机会纠正和重新评估代码。语法错误是在描述步骤中所犯的错误，这些错误相对于底层几何语言的语法是不规则的。语义错误发生在某些情况下，一些结构是不可能的给定点（点的笛卡尔坐标）。演绎错误发生在某些构造总是不可能的情况下（这些错误需要调用证明器）。图9和图10展示了添加代码（在文本区域中）、提交代码进行评估以及以图形方式查看结果和提交的代码的可能性。如果有错误，它们会显示出来，用户可以纠正它们。我们计划合并一个语法突出显示文本编辑器（例如，Helena7）作为textarea字段的替代，以这种方式提供行号和语法高亮。“交互工作”部分可用于在将新结果添加到数据库之前对其进行处理。在下面的文本中，我们将说明用户与GeoThms的交互，例如将中点定理添加到数据库中定理1（中点定理）设ABC为三角形，AJ和BJ分别为AC和BC的中点。 那么直线AJBJ平行于直线AB。使用GeoThms的交互部分，用户可以通过描述构造开始，继续尝试证明猜想，并且如果一切按预期进行，则将所有这些数据以及新的猜想语句插入数据库。描述结构见图9。 中点定理-与DGS的图形的构造性规范必须定义：三个（固定的）点A，B，C（三角形的顶点）;两个（构造的）点AJ和BJ，分别是AC和BC的两个中点，以及所有的注意绘图命令与定理证明器无关，但与生成数字相关（见图9）。该结构是使用GCLC，但7http://helene.muze.nl/44P. Quaresma，P. 《理论与计算科学》电子期刊174（2007）35用户也可以使用Eukleides来描述结构，通过与给定的指令非常相似的指令。检验猜想图10个。中点定理-与ATP的相互作用在从代码中消除所有错误后，用户可以添加推测。的要证明的性质可以用下面的方式表示（使用面积法）SAJBJA=SAJBJB，即，ΔAJBJA的有符号面积等于ΔAJBJB的有符号面积。通过点击适当的按钮，用户从“几何绘图仪”转到GCLC用户现在可以在ATP的代码中添加推测证明{equal {signed_area3 A_1 B_1 A}{signed_area3 A_1 B_1 B}}在此之后，开始新的编写和评估周期（drawers命令已经正确，但推测可能写得不正确）。 之后，用户将得到证明器的输出，其形式为证明状态、包含证明（如果猜想有效）的PDF文件（由GCLCprover生成）以及一些有效性度量。如图10所示，可以访问证明状态和有效性度量，并且证明以PDF文件的形式给出。图11显示了GCLCprover进行证明的最后步骤。将中点定理添加到数据库通过一个新的点击，贡献者可以选择P. Quaresma，P. 《理论与计算科学》电子期刊174（2007）3545（十一）„«1·SACB=（SBAB+SBCB），用代数简化2l l（十二）„«1·SACB2„„=SBAB+„««1·（SBAC+（−1·SBAB））2«+SBCBl、通过引理29（消除点B1（十三）„«1·SACB2„„„««=0+1·（SACB+（−1 ·0））2«+SBCBl、通过几何简化（14）0 = S BCB1，用代数简化(15)0为0„SBCB+„««1·（SBCC+（−1·SBCB））2、通过引理29（消除点B1„ „««(16)0为00+1·（0 +（−1 ·0））2、通过几何简化(17)0 = 0，用代数简化见图11。 中点定理5.5搜索数据库GeoThms6相关工作有几个系统与GeoThms相关。以下工具在某种程度上将DGSs与ATP或定理库联系起来（表1显示了这些工具的功能比较）：几何浏览器结合了DGS的功能与定理证明器的基础上的full-angleme hhMMP/Geometer结合了DGS和ATP的特点，并使用不同的证明方法[10，11]。几何专家（GEX）（新版本，目前正在开发中）是一个具有客户端Web界面的DGS; GEX证明器基于代数证明方法，用户只能从有限数量的结论(e.g.、“三个选定的点是否共线？”）。GEX工具没有可访问的问题数据库，也不提供图像和校样的格式化输出。GEOTHER是一个在Maple中实现的操作和证明几何定理的环境，具有Java中的绘图例程和接口GEOTHER可以使用菜单驱动的图形用户界面，并包含定理在初等和微分几何，与样本规格已被证明。[21、20]。Cinderella使用几何性质的随机定理检查;它不提供任何形式的证明[5，14，19]。Discover是一个可以与Mathematica 8通信的DGS，使用Mathematica 8的符号能力来实现Groéebnerba s esesmethod[2]。有必要将几何结构转换成代数形式并返回，8http://www.wolfram.com46P. Quaresma，P. 《理论与计算科学》电子期刊174（2007）35工具DGSATP可读证明Web界面问题库结构验证GeoThms√√√√√√几何浏览器√√√MMP/几何√√√GEX（旧版本）√√√GEX（新版本）√√√GEOTHER√√√灰姑娘√发现√√几何三角形√√√GeoView√√GeoGebra√定理√√表1结合DGS、ATP和几何定理从代数形式的结论到几何形式的结论。没有提供任何形式的证据。geometriagon在经典几何学（仅限于直尺和指南针）领域有大量的问题。注册用户可以访问/编辑所有问题和解决方案。它不提供ATP。用户可以仅使用有限的一组工具，仅执行构造中的有效步骤，并且以这种方式，系统能够识别用户何时已经达到问题的解决方案。没有提供正式的证据。GeoView将Coq ATP和GeoplanJ DGS结合到一个框架中，在这个框架中可以编辑几何定理的陈述，并使用DGS可视化陈述[1]。这些证据是无法获得的。GeoGebra是一个具有国际化图形界面的DGS，允许图形和文本输入。 数字可以导出为各种格式，包括Web的动态版本。它没有ATP工具，也没有问题的解决[8]。该理论体系综合了多种不同的数学工具和理论，包括基于格若贝内基方法、吴方法、面积方法等的预处理方法该系统建立在Mathematica8系统之上，并使用其可视化工具[3]。7未来工作我们正计划通过其他动态几何工具和其他几何定理证明器来增强框架。我们正在考虑基于全域方法（也产生合成证明），吴的方法和G r o？ebn e r b a s e m e h o d的定理证明器。我们正在努力使数据与这些目标保持一致9geometriagon：http://www.polarprof.net/geometriagon/P. Quaresma，P. 《理论与计算科学》电子期刊174（2007）3547（内部，GeoThms内部和外部）通过我们的XML格式进行几何构造和证明。我们正计划合并一个语法高亮文本编辑器作为textarea字段的替代品，以这种方式提供行号和语法高亮。我们计划使用Math-ML来渲染存储在XML中的定理搜索机制将得到改进，以提供高级搜索选项我们正计划将GeoThms国际化，以使其更广泛地用于教育。“帮助”系统将得到改进，在已经提供的各种帮助网页上增加更详细的8结论GeoThms为用户提供了一个复杂的基于网络的框架，适合于交流几何知识的新方式，它提供了一个开放的系统，人们可以从现有的知识库中学习并寻求新的结果。GeoThms还提供了一个存储几何知识的系统（以严格的声明形式）- 不仅是定理陈述，而且是它们的（自动生成的）证明和相应的证明，即，视觉化我们正计划进一步开发GeoThms，改进其功能并加入更多几何工具。我们也希望GeoThms引用[1] YvesBertot，FrdricGuil hot，anddLocépépottier.Visu alizinggeomistahttp://www-sop.inria.fr/lemme/geoview/geoview.ps、2004年[2] Francisco Botana和Jos L.瓦尔卡斯几何定理发现的动态符号接口计算机与教育，38：21[3] Bruno等人布奇伯格Theorma：Towards Computer-Aided Mathematical Theory Exploration.应用逻辑杂志，2006年。[4] Shang-Ching Chou，Xiao-Shan Gao，and Jing-Zhong Zhang.构造性几何定理传统证明的自动生成。Moshe Vardi，编辑，Proceedings of the Eighth Annual IEEE Symposium on Logic in Computer ScienceLICS，第48-56页。IEEE计算机协会出版社，1993年6月。[5] 灰姑娘网站。http://www.cinderella.de网站。[6] Shang-Ching Chou，Xiao-Shan Gao，and Jing-Zhong Zhang.自动生成可读的几何不变量证明，我。多个和最短的证明生成。Journal of Automated Reasoning，17：325[7] Mirj anaDjori'canddPredragJanibuccici'c. 结构，结构，行动。TeachingMatematics及其应用，23（2）：69[8] 卡尔·福克斯和马库斯·霍恩沃特。动态几何、代数和微积分在软件系统geogebra中的结合。在计算机代数系统和动态几何系统的数学教学会议2004年，佩奇，匈牙利，2004年。[9] 高小山。 盖克斯 http://www.mmrc.iss.ac.cn/http：//www.example.com48P. Quaresma，P. 《理论与计算科学》电子期刊174（2007）35[10] 高小山和林强。几何自动推理软件包在Franz Winkler，编辑，Automated Deduction in Geometry：4thInternational Workshop，（ADG 2002），编号2930 in LNCS，第44-66页。Springer-Verlag，2004.[11] X. S. Gao和Q.是林书 Mmp/geometer.http://www.mmrc.iss.ac.cn/[12] PRDRAGJAIAIBICCAIVANTRAJOVIC。Wingclc-aworkbenchformallyescribingg g ures。在Proceedings ofthe 18 th Spring Conference on Computer Graphics（SCCG 2003），第251-256页中。ACM Press，New York，USA，April，24-26 2003.[13] PredragJanicampaignandPedroQuaresma.系 统 描 述 ： Gclcprover+geothms 。 InUlrichFurbach 和Natarajan Shankar，编辑，IJCAR 2006，LNAI。Springer-Verlag，2006.[14] Ulrich Kortenkamp和Jrgen Richter-Gebert。利用定理自动证明提高几何软件的可用性。数学用户界面研讨会2004年，2004年。[15] 朱利安·纳布coq中的几何判定过程。在Proceedings TPHOLS 2004，卷3223的计算机科学讲义。Springer，2004.[16] 克里斯蒂安·奥布雷希特尤克里德斯 http://www.eukleides.org/。[17] 佩德罗·德雷雷斯马和普雷德拉格·亚尼契奇。构造几何的框架（基于面积法）。2006/001技术报告，科英布拉大学信息学和系统中心，2006年[18] 佩德罗·德雷斯马和安娜·佩雷拉。地理学的视觉化。Gazeta de Matemtica，（151），Junho 2006.[19] Jrgen Richter-Gebert和Ulrich Kortenkamp。交互式几何软件灰姑娘。Springer，1999年。[20] 王东明Geother. http://www-calfor.lip6.fr/GEOTHER/.[21] 王东明Geother 1.1：自动处理和证明几何定理In F.Winkler，编辑，Automated Deduction in Geometry，LNAI第2930期，第194-215页，柏林海德堡，2004年。史普林格出版社[22] 肖恩·威尔逊和雅克·弗勒里奥 结合动态几何，自动几何定理证明和图解证明。在2005年的CNOP会议记录中，2005。