论文部分内容阅读
该文旨在扼要介绍自动化定理证明(ATP)的发展历史与现状。其中,阐述了 ATP 的理论基础、基本原理和研究方向,列举了部分定理证明系统的主要功能和特征,并介绍了在此领域一些主要人物的基本思想和方法。同时,也对四色问题与初等几何定理证明作了简单的讨论。最后,简单介绍了作者在 IBM—PC 机上实现的“格上的定理证明系统—TPSL”,并给出有关程序与算例。
This article aims to outline the history and current status of the development of automated theorem proving (ATP). Among them, the theoretical foundation, basic principle and research direction of ATP are expounded, the main functions and characteristics of some theorem proving system are listed, and the basic ideas and methods of some main characters in this field are introduced. At the same time, a brief discussion is also made on the four-color problem and elementary geometric theorem proving. Finally, we briefly introduce the “theorem proof system on the grid-TPSL” that the author realizes on the IBM-PC, and give the relevant procedures and examples.