随着计算机技术的发展，人工智能技术取得了突破性的进步。机器定理证明是人工智能领域重要的研究课题，到目前为止已经有几种较为成熟的方法，如吴先生的代数法、张景中院士的“消点算法”、基于规则的定理证明等，这些方法与传统的几何命题证明方法不符。如何能够以符合人们传统习惯的方式来解决几何定理机器证明问题成为一个重要的研究课题。20世纪末期语义Web本体理论的出现给本文的研究提供了一个方向，本文通过对本体及其相关理论的研究得到了一种几何定理证明的方法。该方法用本体模型来对几何命题知识进行描述，通过基于本体的Prolog规则来对几何定义、定理和公理进行描述，最后通过知识库推理机来完成几何定理证明。本文主要做了以下三个方面的研究。1、平面几何本体模型构建方法的研究。通过对本体语言的深入研究，得到一种基于语义的几何命题描述方法。将几何命题知识通过本体的类、属性和个体进行描述。本文采用本体语言OWL DL来描述几何命题的逻辑关系，原因是该本体语言具有逻辑推理能力，可以实现基于规则的推理。2、基于本体与规则几何定理证明的研究。本文首先采用上述方法构建平面几何本体模型。其次，用prolog规则对几何定理进行描述。最后将该Prolog规则作用于平面几何本体模型完成几何定理证明。3、几何定理规则半自动生成方法的研究。本文通过对Prolog规则和平面几何本体模型关系的深入研究，总结其对应关系，得到了一种可以自动生成几何定理Prolog规则约束的方法，该方法可以提高规则的书写效率，支持定理可持续证明。最后，本文分别设计了定理规则半自动生成的实验和几何定理自动证明的实验，分别阐述了上述理论在工程角度的可行性，并且对实验的结果进行了分析，进一步验证了上述理论。