几何自动推理是让计算机模拟人脑来进行几何命题的证明，它是人工智能领域的重要研究课题。20世纪70年代，吴文俊先生就提出了定理机器证明的方法；随后，张景中院士在面积法的基础上发展了消点法。这些方法都使自动推理的研究取得了突破性进展。但是，从目前的推理软件来看，关于几何命题的证明还存在一些问题：一是上述方法与传统几何命题的证明方法不符，二是机器还不能完全学会几何学家的解题技巧，如辅助线、辅助点的添加。如何设计一种自动推理的方法，使其在保证效率的前提下，既能符合传统证明方法，又能与几何学家相媲美，成为当前重要的研究课题。为了实现自动推理，本文引入了语义网的相关理论与技术，首先，使用本体对平面几何证明过程和推理规则进行构建，生成本体模型，然后，通过模型匹配，并借助辅助信息库的查询来实现自动推理。主要研究内容如下：1、平面几何知识表示。首先，通过对几何命题证明过程的深入研究，自动化地对每一个因果分段进行概括模型和详细模型的提取，并将模型存储于过程本体中。其中，概括模型体现了因果分段的抽象化描述，详细模型体现了因果分段的实例化描述。接着，为了解决辅助线、辅助点的相关问题，对几何推理规则进行了深入研究，使用Protégé构建了基于平面几何学科知识的领域本体，该领域本体为辅助信息库提供相关信息。2、平面几何知识推理。针对不需要辅助信息就能完成的几何证明，为了提高效率，先使用逆向推理，通过与概括模型的匹配来判断是否可能有解，在条件成立的情况下，再使用正向推理，通过与详细模型的匹配来获得证明过程。针对需要辅助信息才能完成的证明，将通过辅助信息库的查询来获取新条件，以此来增大推理成功率。为了提高推理效率，关于辅助线的添加，在辅助线信息库中只存放不存在连线生成的新条件，而关于辅助点的添加，则根据解题经验设计相关算法，并采用边添加边删除的策略。最后，本文通过实验展示了过程本体与领域本体的构建，并将其成功地应用于需要添加辅助线、辅助点才能解决的自动推理实例中。