自动化定理证明的发展与现状

The Development and Present Situation of Automated Theorem—Proving

该文旨在扼要介绍自动化定理证明(ATP)的发展历史与现状。其中,阐述了 ATP 的理论基础、基本原理和研究方向,列举了部分定理证明系统的主要功能和特征,并介绍了在此领域一些主要人物的基本思想和方法。同时,也对四色问题与初等几何定理证明作了简单的讨论。最后,简单介绍了作者在 IBM—PC 机上实现的“格上的定理证明系统—TPSL”,并给出有关程序与算例。

The purpose of this paper is to introduce the development and present situation of ATP briefly.The theoretical basis,main principles and re-search directions of ATP are described.The functions and features of certain provers are also listed.Meanwhile,the thoughts and methods of some great contributors to ATP are given in the paper.Additionally,the well—known four colour problem and elementary geometry theorem—proving problem have been discussed.Finally,an implementation,of a Theorem Proving System on Lattice—TPSL on IBM—PC,by authors,and the program written in PROLOG as well as some examples are presented.