当我们阅读几何书本上的证明的时候,通常需要花费相当的时间和精力来辨识证明文本中的几何元素和几何图形的对应关系。当几何图形或者证明变得复杂的时候,这个问题就会变得很严重。因此,如何在计算机中重新组织和表示几何证明使得它们更容易阅读和理解将是一件十分有意义的事情,这也是证明可视化研究的主要课题之一。本文对平面几何证明可视化方面目前存在的问题进行了深入的研究,其中最主要的是动态几何技术,可读证明的产生、组织以及显示技术等。本文的主要研究目标是为平面几何研究和设计一套能够高效地输入、产生以及表示证明的技术,以帮助用户更好地理解证明。具体的研究内容可以分为以下三个方面：1.研究高效率的方法处理几何图形中的约束关系。几何图形在几何定理的证明过程中起着非常重要的作用。给定一个几何定理,画出其图形并对该图形进行变换的过程可以看做是一个约束求解的过程。传统的约束求解方法没有对约束进行统一的处理,因此在求解效率,稳定性等方面都存在不小的问题。本文研究了如何开发高效的算法对几何图形的约束关系进行求解,希望通过利用平面几何定理的一些特殊性质,能够借助强大的代数方法来求解几何图形中的约束关系。2.研究了专门用于几何定理证明可视化的技术以及输入工具。证明文本和几何图形的对应关系是证明可视化技术的关键。但是对于传统的可读证明来说,这两者是分开的,需要读者在阅读的过程中去比较、识别它们之间的关系。对此,本文研究了平面几何证明的语法结构,希望能够给出几何证明的一般性的结构和组织方式,并且针对这种格式化的证明提出一种可视化方法,使得我们能够把证明文本和证明图形对应起来。另外,本文研究了可视证明的不同产生方法：一方面,考虑提供手动的交互式证明输入工具,让用户使用图形化的工具建立证明。另一方面,考虑提供自动化的方法,充分利用当前几何定理机器证明领域的研究成果,使得用户只需要输入定理文本形式的前提条件就能够自动地产生几何图形以及可视证明。3.研究了动态可视证明的自动产生方法以及证明的层次型组织结构。对于一个复杂的几何定理,当它的证明包含了很多步骤时,如果能够合理组织证明结构,使得证明能够保持在合理的长度之内,对证明的理解显然非常有帮助。对此,本文研究了可读证明的自动产生以及组织方法,希望能够把证明主要的步骤列出来的同时,把次要的步骤隐藏起来,使得用户在阅读时可以抓住证明的重点。本文对以上问题进行了深入研究,并且获得了一系列研究成果。下面是本文的主要贡献和创新点：1.提出了基于构造型几何命题的几何约束求解方法,利用代数方程高效地表示和处理几何图形的约束关系。对于构造型几何命题,根据几何命题中点引进的顺序依次给点的坐标参数赋值,然后把图形中的约束条件转化成代数方程组,该方程组可以很容易地三角化。根据三角化以后的结果,我们可以高效地对图形中的约束进行求解。相比较传统的几何约束处理方法,该方法具有许多优点,例如求解稳定,可以计算出图形的多种可能情况,并且可以对几何图形的一些隐含的性质进行推理和证明等。2.提出了新的基于几何图形的证明表示方法-动态可视证明,提出了几何定理证明的一般语法结构,并且基于这种结构开发了动态可视证明的手动输入方法。动态可视证明最主要的特征是证明的文本和图形的紧密结合。在手动输入方法中,证明的语法结构经过了严格的定义,并且根据这种格式化的证明,采用以鼠标操作为主的输入方式,使得用户可以在事先知道具体证明的情况下很容易地输入动态可视证明。3.提出了基于无序几何模型的动态可视证明自动产生方法：基于全角法的产生方法和基于演绎数据库法的产生方法。这两种方法都是基于无序几何的,非常适合算法实现并且生成动态可视效果。而且,在全角法中,通过结合前推法和后推法,我们提出了证明的层次型组织方法。这种方法使得用户可以把注意力集中在主要的步骤上,而当用户对某些步骤的进一步证明感兴趣时,又可以展开这些步骤,查看它们的详细证明。在演绎数据法中,我们产生一个包含该几何定理的许多信息的数据库,且成功地实现了数据库的可视化。4.基于前面研究成果,我们构造了一款几何定理证明器:Java Geometry Expert (JGEX)。JGEX是一款集成了几何作图、证明以及证明的动态显示为一体的几何软件,它最重要的特性就是实现了我们上面所提到的动态可视证明技术,并且它还提供了手动和自动两种方法产生动态可视证明。利用这些技术,我们已经成功地产生了两百多个动态可视证明的例子。这些技术和例子不仅可以被用于中学几何教学,也可以成为人们学习和研究平面几何证明的有力工具。