现有的几何自动推理系统采用较多的是基于单向推理法(包括前向推理和后向推理)的搜索方法.单向推理尤其是前向推理法已经取得了显著的成就,如z+z智能教育平台的系列软件《平面几何》、《立体几何》等就是基于前推法的自动推理系统.随着对平面几何自动推理研究的不断深入,对推理效率提出了更高的要求.为了进一步提高平面几何自动推理系统的效率,该文探讨了将前推法与后推法结合起来进行平面几何推理的方法.从该系统的实际测试情况看,尤其是对较为复杂的几何问题,采用它可以显著提高推理效率.文章首先对机器证明简史进行了回顾,然后对系统作了总体介绍,说明了谓词和规则的选取.文中第三章是全文的核心部分,详细介绍了作者的工作思路.第一节分析了各种常见的推理策略及其优缺点,引出双向推理方法,并着重分析了后推的重点和难点、可能遇到的问题以及解决办法;第二至六节对双向推理系统模型、工作过程等进行了描述,指出双向推理系统的程序主要包括三个类:信息类,引理类和推理类,其中推理类是整个系统的核心程序.第七节介绍了对用户输入的可识别处理方法;第八节详细说明了几个关键技术的实现等;第九节介绍了为提高推理效率所采用的一些方法.在第四章中作者对该系统中的一些不完善之处及今后可能的改进做了简要的阐述和展望.附录给出了采用该系统进行平面几何自动推理的一些例题.