汤晓凌[1]2005年在《集合论等式型定理机器证明系统的研究与开发》文中研究说明定理机器证明的研究已有将近50年的历史,并已经在数理逻辑、初等代数和几何学等学科取得显着成功。关于集合论的定理机器证明研究,有关文献报道用布尔代数的方法可以把集合论的定理证明问题转化为代数问题,但是这类问题的可读证明方法,目前尚未查到有关报道。许多国内外的着名数学软件中,集合论等式型定理的推理方面的功能也比较弱。本论文以人工智能中的搜索算法为基础,研究集合论等式型定理可读证明的机械化方法。 本课题所做的工作包括: 1、通过比较各种搜索算法,选择了盲目搜索算法中渐进最优的迭代加深算法构建推理树,并作了必要的改良,以加速搜索路径的产生。 2、通过研究手工证明和专家经验,总结出几条启发式的规则引导搜索:根据使用频率将公式重新排序;添加了公式反向使用规则;判断左右式长短以决定证明方向;分析结果倒序进栈以保证大的匹配结果优先扩展。 3、利用编程语言Lisp的特点,寻找了一些适合计算机处理的方法,如推理的内部数据用前缀形式。 4、使用了一些方法加速调试,如:先用其他易输入的半角符号代替难输入的全角集合运算符,调通程序;先缩小规模,验证程序的执行过程;运用注解方便测试与修改;如果真实数据过于复杂或难以获得,第一遍采用仿真数据测试,将复杂结果与变量输出到文件监视。 5、采取一些措施,产生详细推理说明。在每一步代换推理前,记录所用的规则以及使用该规则的理由。 6、通过比较数理逻辑和集合论相关的规则,将定理分类推理,基本定理作为经验常识,直接输出结果,不需要说明,加快了证明速度。这一设计可以让宏运算不必都化成基本定理推理,简化证明过程。 本文前叁章介绍本课题所涉及的相关的理论以及本文工作构想。第四章引入易于分析和设计修改的PAD图,介绍主程序和处理边界问题的程序。第五章以系统的叁个核心程序为例,用可以推广的方式探讨了调试技巧。最后作者指出了本文工作进一步努力的方向:增加搜索策略的灵活性、启发函数和学习功能以及研究规则库和搜索策略的动态调整方法。
叶征[2]2010年在《平面几何的动态可视证明研究》文中研究表明当我们阅读几何书本上的证明的时候,通常需要花费相当的时间和精力来辨识证明文本中的几何元素和几何图形的对应关系。当几何图形或者证明变得复杂的时候,这个问题就会变得很严重。因此,如何在计算机中重新组织和表示几何证明使得它们更容易阅读和理解将是一件十分有意义的事情,这也是证明可视化研究的主要课题之一。本文对平面几何证明可视化方面目前存在的问题进行了深入的研究,其中最主要的是动态几何技术,可读证明的产生、组织以及显示技术等。本文的主要研究目标是为平面几何研究和设计一套能够高效地输入、产生以及表示证明的技术,以帮助用户更好地理解证明。具体的研究内容可以分为以下叁个方面：1.研究高效率的方法处理几何图形中的约束关系。几何图形在几何定理的证明过程中起着非常重要的作用。给定一个几何定理,画出其图形并对该图形进行变换的过程可以看做是一个约束求解的过程。传统的约束求解方法没有对约束进行统一的处理,因此在求解效率,稳定性等方面都存在不小的问题。本文研究了如何开发高效的算法对几何图形的约束关系进行求解,希望通过利用平面几何定理的一些特殊性质,能够借助强大的代数方法来求解几何图形中的约束关系。2.研究了专门用于几何定理证明可视化的技术以及输入工具。证明文本和几何图形的对应关系是证明可视化技术的关键。但是对于传统的可读证明来说,这两者是分开的,需要读者在阅读的过程中去比较、识别它们之间的关系。对此,本文研究了平面几何证明的语法结构,希望能够给出几何证明的一般性的结构和组织方式,并且针对这种格式化的证明提出一种可视化方法,使得我们能够把证明文本和证明图形对应起来。另外,本文研究了可视证明的不同产生方法：一方面,考虑提供手动的交互式证明输入工具,让用户使用图形化的工具建立证明。另一方面,考虑提供自动化的方法,充分利用当前几何定理机器证明领域的研究成果,使得用户只需要输入定理文本形式的前提条件就能够自动地产生几何图形以及可视证明。3.研究了动态可视证明的自动产生方法以及证明的层次型组织结构。对于一个复杂的几何定理,当它的证明包含了很多步骤时,如果能够合理组织证明结构,使得证明能够保持在合理的长度之内,对证明的理解显然非常有帮助。对此,本文研究了可读证明的自动产生以及组织方法,希望能够把证明主要的步骤列出来的同时,把次要的步骤隐藏起来,使得用户在阅读时可以抓住证明的重点。本文对以上问题进行了深入研究,并且获得了一系列研究成果。下面是本文的主要贡献和创新点：1.提出了基于构造型几何命题的几何约束求解方法,利用代数方程高效地表示和处理几何图形的约束关系。对于构造型几何命题,根据几何命题中点引进的顺序依次给点的坐标参数赋值,然后把图形中的约束条件转化成代数方程组,该方程组可以很容易地叁角化。根据叁角化以后的结果,我们可以高效地对图形中的约束进行求解。相比较传统的几何约束处理方法,该方法具有许多优点,例如求解稳定,可以计算出图形的多种可能情况,并且可以对几何图形的一些隐含的性质进行推理和证明等。2.提出了新的基于几何图形的证明表示方法-动态可视证明,提出了几何定理证明的一般语法结构,并且基于这种结构开发了动态可视证明的手动输入方法。动态可视证明最主要的特征是证明的文本和图形的紧密结合。在手动输入方法中,证明的语法结构经过了严格的定义,并且根据这种格式化的证明,采用以鼠标操作为主的输入方式,使得用户可以在事先知道具体证明的情况下很容易地输入动态可视证明。3.提出了基于无序几何模型的动态可视证明自动产生方法：基于全角法的产生方法和基于演绎数据库法的产生方法。这两种方法都是基于无序几何的,非常适合算法实现并且生成动态可视效果。而且,在全角法中,通过结合前推法和后推法,我们提出了证明的层次型组织方法。这种方法使得用户可以把注意力集中在主要的步骤上,而当用户对某些步骤的进一步证明感兴趣时,又可以展开这些步骤,查看它们的详细证明。在演绎数据法中,我们产生一个包含该几何定理的许多信息的数据库,且成功地实现了数据库的可视化。4.基于前面研究成果,我们构造了一款几何定理证明器:Java Geometry Expert (JGEX)。JGEX是一款集成了几何作图、证明以及证明的动态显示为一体的几何软件,它最重要的特性就是实现了我们上面所提到的动态可视证明技术,并且它还提供了手动和自动两种方法产生动态可视证明。利用这些技术,我们已经成功地产生了两百多个动态可视证明的例子。这些技术和例子不仅可以被用于中学几何教学,也可以成为人们学习和研究平面几何证明的有力工具。
闫丽慧[3]2007年在《基于网格计算的定理自动证明研究》文中研究说明自动定理证明(又叫机器定理证明、机械化定理证明等)是人工智能研究的一个重要分枝,是数学、计算机科学的交叉学科,我国科学家在这一领域的研究走在了世界的前列。不仅提出了多种有效的方法,还成功的开发了一些智能的定理证明系统,其中一些成果已经被成功的应用到几何教育领域。但当前机器证明的理论研究进入低潮,自20世纪末以来,国外研究人员尝试将网络并行计算技术引入到一些关键计算问题中,以求得较高的计算效率,国内这方面的研究也处于起步阶段。近年来,随着Web技术的日益发展和Internet的广泛应用,越来越多的人开始研究借助网络解决数学问题,目前绝大部分研究都是以数学信息平台的建设作为重点,在远程和分布式的环境下实现定理的自动证明的研究并不多见。网格计算是新一代的分布式计算方法,用来表述一种适用于高端科学和工程的分布式计算的体系结构。与传统分布式计算的主要区别在于在没有集中控制机制的情况下,通过对计算资源进行大规模共享,满足应用对高性能计算要求,并且这种对计算资源进行大规模共享是动态的、柔性的、安全的和协作式的,解决了常见的网络并行计算系统面临的操作系统、协议的异构性问题。如果将网格计算的技术应用到几何定理证明的方法中,就可以利用网格提供的超级计算能力,实现高效的协作资源共享,提高定理系统的可重用性、交互性及定理证明的效率。本文的工作是以几何定理证明中的数值方法为基础,尝试将网格计算技术应用于几何定理自动证明,探究一种基于网格计算的几何定理证明的实现方法。在充分分析了网络并行计算理论和实现技术的基础之上,提出了针对数值并行法的网格并行计算虚拟模型。并结合网格环境下数值并行计算实现的难点,采用概率性方法对其加以改进,使得该方法在实现时更加简洁、高效,也为网格计算技术在定理自动证明方面的应用、构建基于网格服务的数学系统方面提供了有益的借鉴。
陈明雁[4]2014年在《基于概率检测组合模型的几何定理证明器》文中提出几何定理机器证明是指通过机器自动地证明几何定理,常用的证明方法可分为叁类：代数法、向量法以及基于推理数据库的搜索法。上述叁类方法都属于确定性方法,即只要按正确的步骤计算执行,总能得到确定性的结果。然而,当涉及到复杂问题时,确定性方法的复杂度会偏高,从而严重影响到解题的效率。于是,便有了与“确定性”方法相对应的能够高效执行的“概率性”方法。为此,国外已有研究学者开始探索概率性方法在几何定理机器证明的应用,并取得了一定的成效。但是目前国内尚未有人对概率性方法进行研究,并且已有的确定性方法和概率性方法尚存在复杂度过高或者对非线性类构造性几何定理的证明力度偏弱等问题。本文针对已有的确定性方法和概率性方法的证明速率偏低或占用内存过大等问题,从代数簇构造理论出发,对几何定理机器证明的概率性方法做了以下研究工作：(1)提出一种改进的估算余式次数上界的算法。分析构造性几何定理的多项式组代数簇的不可约分解的基本特点,在此基础上提出了一种改进的估算余式R(结合假设部分的多项式组消去结论部分多项式的全部约束变元后得到的只含独立变元的多项式)关于每个独立变元次数的上界的快速算法。在改进的算法的基础上,成功推导出构造性几何定理的余式R关于每个独立变元次数的上界满足Bound1=O(30[n/2])。此外,若定理限制为线性类的构造性几何定理,则还可将其上界改进为Bound2=O(3n)。(2)提出叁种统计总体采集标准。在改进算法和相关推论基础上,结合Schwartz-Zippel定理和统计学理论,提出了叁种不同的具有一定针对性和适用范围的统计总体采集标准。其中,第一和第二种采集标准是基于改进的算法提出来的,而第叁种则是针对改进算法的推论提出来的,二者具有不同的适应范围。在实验部分,我们还设计了对比实验对这叁种采集标准的适用范围进行分析和评价。(3)比较分析两种实例检验方法。给出两种不同的随机实例检验方法,即数值检验法和连续伪除检验法。文中还进一步探讨了这两种检验方法对退化情况及多项式组可约性情况的处理方法。最后还结合多组对比实验数据对这两种不同的检验方法的适用性进行评价。(4)开发基于概率检测组合模型的几何定理证明器——-ProbProvero在上述理论研究和分析的基础上,本文还进一步设计了概率检测组合模型并对模型进行了显着性检验及统计错误分析。进一步地,我们采用Maple编程语言实现此基于概率检测组合模型的几何定理证明器——ProbProver。通过ProbProver证明器,我们成功在2秒内证明了代数法难以证明的Five Circles和Miquel定理。为了进一步证实本文提出的基于概率检测组合模型的几何定理证明器具有一定的高效性,本文从多个维度出发,对若干个复杂程度不尽相同的几何定理进行了多组重复实验。实验数据表明,本文提出的基于概率检测组合模型的几何定理证明器具有显着的高效性,并具有一定的应用前景。
尤枫[5]2003年在《几何定理机器证明系统的开发与研究》文中研究表明通常,几何定理的证明是依据公理系统,按一定的逻辑规则演绎地进行。对于每一个定理,其证明的方法都是不同的,一种方法只适用于一个定理,没有通用的证明方法或指导思想适合于所有的定理哪怕是某一类定理,证明方法不能触类旁通,只能凭借经验和严密的逻辑判断能力来进行。随着20世纪70年代吴文俊先生关于数学机械化方法的创立,使得机械化证明和计算在数学的许多领域才成为现实。这一被称为吴方法的数学机械化方法,特别在几何定理机械化证明中得到了很好的应用。这是基于构造性的代数几何理论的一种证明方法,使得证明可以沿着一条有规律的刻板的道路进行,为几何定理的证明开辟了新的途径。本文围绕数学机械化的吴方法展开了对初等几何机械化证明的探讨和研究,主要内容包括:(1)以Maple和Matlab系统为支撑开发了运用该方法证明定理的软件系统。(2)对大量的定理进行了实验性证明。(3)对采用该方法进行证明时存在的问题进行了研究。
丁盘苹[6]2012年在《基于本体和Prolog规则的几何定理证明的研究》文中研究说明随着计算机技术的发展，人工智能技术取得了突破性的进步。机器定理证明是人工智能领域重要的研究课题，到目前为止已经有几种较为成熟的方法，如吴先生的代数法、张景中院士的“消点算法”、基于规则的定理证明等，这些方法与传统的几何命题证明方法不符。如何能够以符合人们传统习惯的方式来解决几何定理机器证明问题成为一个重要的研究课题。20世纪末期语义Web本体理论的出现给本文的研究提供了一个方向，本文通过对本体及其相关理论的研究得到了一种几何定理证明的方法。该方法用本体模型来对几何命题知识进行描述，通过基于本体的Prolog规则来对几何定义、定理和公理进行描述，最后通过知识库推理机来完成几何定理证明。本文主要做了以下叁个方面的研究。1、平面几何本体模型构建方法的研究。通过对本体语言的深入研究，得到一种基于语义的几何命题描述方法。将几何命题知识通过本体的类、属性和个体进行描述。本文采用本体语言OWL DL来描述几何命题的逻辑关系，原因是该本体语言具有逻辑推理能力，可以实现基于规则的推理。2、基于本体与规则几何定理证明的研究。本文首先采用上述方法构建平面几何本体模型。其次，用prolog规则对几何定理进行描述。最后将该Prolog规则作用于平面几何本体模型完成几何定理证明。3、几何定理规则半自动生成方法的研究。本文通过对Prolog规则和平面几何本体模型关系的深入研究，总结其对应关系，得到了一种可以自动生成几何定理Prolog规则约束的方法，该方法可以提高规则的书写效率，支持定理可持续证明。最后，本文分别设计了定理规则半自动生成的实验和几何定理自动证明的实验，分别阐述了上述理论在工程角度的可行性，并且对实验的结果进行了分析，进一步验证了上述理论。
江建国[7]2006年在《iGeo：智能几何软件的定理证明器》文中提出动态几何软件(Dynamic Geometry Software)与普通的作图软件有着本质上的不同。它绘制的几何图形不但精确,而且还具有动态性,这使其非常适合于几何教学的实际需要。动态几何软件已经成为了几何教学的强有力工具,对几何教学的现代化改革产生了重大而又深远的影响。然而,教育的实际应用也逐渐暴露了动态几何软件的很多缺陷。其主要缺陷是动态几何不具有智能性。缺少智能性是制约动态几何软件有效应用的瓶颈。这里,智能性是指动态几何软件能象“几何专家”一样帮助用户解题。本文把这种具有专家级解题能力的动态几何软件称为智能几何软件(IntelligentGeometry Software)。智能几何软件不但能动态作图而且还能自动解题。这使其能更好地帮助学生学习几何证明。应用几何定理机器证明的研究成果,可以研制出高智能的几何教育软件。这只需在动态几何软件中嵌入一个定理证明器,就可以简单地实现具有专家级解题能力的智能几何软件。目前,研制成功的智能几何软件已经走进了中学几何教学的课堂,比如《几何专家》,《超级画板》,《体验数学—Math Xp》等等。定理证明器是智能几何软件的推理引擎的核心程序。大多数智能几何软件都使用基于前推法(forward chaining method)的定理证明器作为推理引擎。这是因为前推法能给出易于学生理解、易于检验的传统证明。但是,前推法还存在着有很多不足,比如推理效率比较低,解题能力有很大的局限性。为了进一步提高前推法的推理效率和增强前推法的解题能力,以便使智能几何软件能更好地满足几何教学的实际需要,本文针对前推法提出以下3种改进技术:1.将Rete模式匹配算法整合到前推法的推理引擎中,构造了一种具有高匹配效率的前推法推理引擎。本文把这种推理引擎为几何自动推理网。几何自动推理网把规则集转换成数据流网,用数据流网来动态地保存推理规则和几何信息的匹配状态。通过消除推理过程中冗余匹配来提高推理效率。2.为了提高前推法对几何等价信息的推理效率,提出了一种高效的等价类推理方法。该方法包括两种技术:(1)使用等价类合并推理规则替换等价谓词的传递推理规则。(2)使用等价类代换推理规则替换等词的代换推理规
沈盈[8]2008年在《构造性和非构造性几何命题证明方法》文中研究指明定理机器证明是人工智能研究的一个重要课题,在其中的几何定理机器证明研究领域,我国的科学家最近二十几年来取得了一系列令世人瞩目的成果,提出了消点法、吴方法、几何不变量法、演绎数据库的搜索法,以及数值并行法等多种不同的方法。基于这些方法设计开发的几何定理证明系统不仅推动了人们对几何领域问题的研究,也为其它领域的定理自动证明提供了有益的启示。目前已有的几何定理证明方法大多只侧重于几何定理的严格证明,然而人们研究几何问题时会发现,除了严格证明之外,一个几何问题是否还可以用其他不怎么严格的方法来证明。有时人们感兴趣的不是它的证明过程而是证明过程中的某些几何关系。它不但有助于命题结论的证明,而且便于人们更深入透彻的理解整个几何命题,甚至可以从中发现新的未知的定理。此外,几何定理自动证明在实现方面尚有一些需要探索改进的地方,例如进一步提高证明的效率,以及解决非构造性命题等。针对这些问题,本文在数值方法的基础上提出了几何定理的动态搜索方法。在此基础上,我们结合非构造性几何命题的特点对该方法进行了改进,使其同样能够解决非构造性的初等平面几何命题,扩展了方法的应用范围。此外,我们还运用消点法证明了一些构造性和非构造几何命题,扩展了这一方法在非构造性几何命题方面的应用。
王建林[9]2012年在《基于Isabelle平台的一般拓扑学机械化及自动定理证明研究》文中提出数学机械化是以构造性和算法化的方式来研究数学问题,使这些数学问题的计算、推理或证明可机械化甚至自动化地完成。数学问题的机械化,即要求在运算或证明过程中,每前进一步之后,都有一个确定的、必须选择的下一步,按照一条有规律的、刻板的方式,最后得出结论。数学机械化中一个重要的任务是定理机器证明,即研究如何应用计算机程序来证明数学定理,具体地说,如何通过一套符号体系将人脑的推理证明过程形式化,从而转化为一系列可在计算机上自动实现的推理证明过程。拓扑学是近代发展起来的一个研究连续性现象的数学分支。拓扑学主要研究拓扑空间在拓扑变换下的不变性和不变量,是现代数学研究的理论基础之一。拓扑学不仅在数学的其他分支有着重要作用,而且在其他诸如物理、化学、经济、生物等学科中也发挥着重要的作用。拓扑学机械化能为这些学科的发展提供机械化的理论工具,拓扑学机械化也是数学机械化自身发展的需要。但由于拓扑学的研究对象十分抽象其在计算机系统中的表达非常困难,因而以往的定理机器证明或者数学机械化的研究较少涉及拓扑学这个领域。随着计算机技术的飞速发展,计算机定理证明工具的不断丰富及发展为实现拓扑学的定理机器证明带来了契机,Isabelle就是定理证明工具中的佼佼者。Isabelle使用自然演绎规则进行推理,为定理证明系统的开发提供了一个通用的框架。它既支持数学公式的形式化描述,又为公式的逻辑演算提供了证明工具。Isabelle具有丰富的表达能力、灵活高效的命令集、强大的规则库和灵活且易于扩展的策略库,而且其句法易于扩展,证明过程的可读性强,自动化程度高。一般拓扑学是拓扑学的一个基础分支,为其它的拓扑学分支如代数拓扑、几何拓扑、微分拓扑提供了共同的基础。本论文主要围绕着一般拓扑学机械化展开,主要工作包含以下叁个部分：第一、基于Isabelle的一般拓扑学机械化。本文采用高阶逻辑的形式语言来表达一般拓扑学中诸如拓扑空间、开集、闭集、邻域、闭包、连续函数等抽象概念,并将这些抽象概念表示为可计算函数形式,使得这些抽象的数学对象能在Isabelle中以λ-演算的形式实现演绎推理。此外,针对计算机可处理的数学对象,详细研究了证明策略序列的构造方法和技巧,如引入策略、重写策略、分类策略等,并采用逐步求精的方式,实现相关的定理机器证明。论文还实现了一般拓扑学中一些基本定理的机器证明,包括黏结引理、Kuratowski定理、杨忠道定理等涉及复杂集合运算的定理机器证明。第二、在机械化一般拓扑学研究基础上,本文使用Isabelle来表达拓扑动力系统所涉及的基本概念,其中包括群、拓扑群、拓扑迁移群等。并从拓扑迁移群的视角对拓扑动力系统进行研究,并实现了相关定理的机器证明。最后,归纳总结了这些定理的机械化证明方法。第叁、形式化定理证明工具的实现。本文基于Isabelle开发了一个自动发现与帮助发现定理的机器证明脚本工具—IsabelleHelper。这一工具本质上是一个定理机器证明的专家系统。它不仅建立了数学定理库和定理证明策略库(或定理证明方法库),而且按照公式间的距离对策略库进行分类和排序,从而极大地缩小了搜索空间,提高了证明效率。IsabelleHelper通过对策略库的搜索、匹配、组合等方法来自动发现定理的机器证明,并为使用者提供不同程度的证明帮助,如完整的定理证明脚本生成、下一步证明的提示等。此外IsabelleHelper通过数学服务总线的方式集成了Isabelle和Maple。由于Isabelle是一个类型系统,侧重于定理验证和推理证明,但对于涉及复杂代数计算的推理较为繁琐；而Maple是一个侧重于符号计算的计算机代数系统,能进行灵活、高效的计算及推理,但由于没有统一的验证机制,可能导致错误或无效的证明。因此本文结合这两大工具的优点,基于开源SOA框架Mule实现了Isabelle和Maple的集成,该集成工具进一步提高了定理证明系统的自动证明能力,扩大了定理证明系统的证明范围。
葛强[10]2011年在《限制条件下的几何自动推理及应用研究》文中进行了进一步梳理几何学具有悠久的历史,两千多年来积累下来的几何知识是人类的宝贵财富。其中,几何证明是几何学的精华之一。几何题的证法,没有统一的方法可依循,有赖于个人的灵感和技巧,一直是数学教学中的难点和重点内容。用机器来模仿人的思维活动,来帮助人证明几何命题,是历史上一些卓越科学家的梦想,也是具有重要研究价值和应用价值的研究方向。吴文俊建立的数学机械化方法,极大的推动了几何定理机器证明领域的研究。目前,基于不同推理算法的自动推理系统已经出现,在科学研究和工程计算中发挥着重要的作用。但是,几何定理自动推理领域中的丰富成果,在教育中并没有得到充分应用,其教育价值远远没能得到充分体现。原因一方面在于中学教育阶段涉及到的几何知识比较初等,而现有的几何自动推理方法给出的证明过程难于被中学生理解；另一方面,几何知识的教学又涉及语言表达与作图、从图形发现问题、问题分析与解答等多个方面,不仅仅是单纯的几何定理机器证明。面对中学几何教学的应用需求,几何自动推理的研究面临着中学几何知识范围、解答步骤长度、推理时间和推理方法等多方面的限制。针对这些限制条件,本文开展了面向中学几何教学的几何自动推理的研究工作,涉及几何自动推理在动态几何作图、几何问题生成、向量法解题等方面的理论方法与应用,研究成果(创新点)包括以下几个方面：第一：提出动态几何作图中的枢点概念,建立了以枢点为基础的动态几何机制,设计了包括智能作图方法,语义作图方法和文本作图等几何作图方法。实现了相应的动态几何作图系统,拓展了动态几何理论。第二：提出并实现基于向量法的自动推理算法。该自动推理方法基于向量的回路特征,对构造型交点类几何命题能迅速地给出可读的向量式证明,证明过程简洁优美。这种自动推理方法能够在限制条件内能达到推理不动点,在构造型交点类的题目上表现出较高的效率。第叁：提出并实现了基于自动推理的几何问题自动生成与答案验证方法。以自动推理为基础,设计了可以生成填空、判断、选择、计算和证明等多种题型的自动出题方法,并实现对用户的解答进行实时验证。这种方法创新了几何学出题方式,提高了测试效率。综合应用上述研究成果,实现了一个面向中学教学应用的几何自动推理原型系统,其主要功能包括动态几何作图、几何自动推理和题目自动生成。这叁种主要功能有机集成,可满足教师课堂教学和学生课下自学的需求。最后提出了值得进一步研究的问题和对此方向未来的展望。
参考文献：
[1]. 集合论等式型定理机器证明系统的研究与开发[D]. 汤晓凌. 华东师范大学. 2005
[2]. 平面几何的动态可视证明研究[D]. 叶征. 浙江大学. 2010
[3]. 基于网格计算的定理自动证明研究[D]. 闫丽慧. 华东师范大学. 2007
[4]. 基于概率检测组合模型的几何定理证明器[D]. 陈明雁. 华东师范大学. 2014
[5]. 几何定理机器证明系统的开发与研究[D]. 尤枫. 北京化工大学. 2003
[6]. 基于本体和Prolog规则的几何定理证明的研究[D]. 丁盘苹. 电子科技大学. 2012
[7]. iGeo：智能几何软件的定理证明器[D]. 江建国. 中国科学院研究生院（成都计算机应用研究所）. 2006
[8]. 构造性和非构造性几何命题证明方法[D]. 沈盈. 宁波大学. 2008
[9]. 基于Isabelle平台的一般拓扑学机械化及自动定理证明研究[D]. 王建林. 华东师范大学. 2012
[10]. 限制条件下的几何自动推理及应用研究[D]. 葛强. 华中师范大学. 2011
标签：计算机软件及计算机应用论文; 代数基本定理论文; 图形推理论文; 命题逻辑论文; 基础数学论文; 概率计算论文; 智能机器论文; 数学论文; 动态模型论文; 拓扑学论文; 推理论文; 代数论文; 科技新闻论文;