定理证明中的三个速算法

定理证明中的三个速算法 THREE FAST ALGORITHMS FOR THEOREM PROVING 李卫华 Li Weihua first-author 作者在曾宪昌教授的指导下,在PDP-11微型机上通过多次实验后,对用归结原理进行定理证明的三个传统算法——合一、归结、包括,进行了改进,从而设计出三个相应的速算法。实验数据表明:对同一种用来进行定理证明的归结原理,引进这三个速算法后,可使证明时间节省数倍。而且要证明的定理愈复杂,效率愈显著。至今,用我们设计的定理证明器TPP已经对《数论》、《群论》、《平面几何》等方面的一些数学定理,以及一些程序正确性的问题在机器上予以自动证明。在速度很慢的微型机上,所通过的定理的证明平均只需30秒的机器时间,其中包括BASIC解释程序所耗时间。 Through a number of experiments on micro computer PDP—11—03, the author has improved the three traditional algorithms—unification, resolution and subsumption, and found three corresponding fast algorithms. As the experimental data demonstrated, the running time can be saved by the three fast algorithms and only 1/3—1/4 of the traditional running time is needed. In addition, the more complex the theorem is, the more the running time can be saved. 1) Fast Unification Algorithm FUA （E 1 E 2 ） is defined to find out a most general unifier of the expressions E 1 and E 2 . If E 1 and E 2 are not unifiable then it returns NO; otherwise, the most general unifier of E 1 and E 2 is （（t 1 v 1 ） …（t n v n ））. 2) Fast Subsumption Algorithm FSA （C 1 C 2 ） is defined to test whether a unit clause C 1 subsumes another unit clause C 2 . 3) Fast Resolution Algorithm FRA （C 1 C 2 N） is defined to resolve two clauses C 1 and C 2 , where C 1 is a unit clause, C 2 is a clause and N+1 is the ordinal number of the new resolvent. 1981-01-01 2021-04-01 1