该文运用Robinson的归结原理,分别用Prolog与Lisp实现了两个格上的定理证明系统——TPSL1和MTPSL2。其中,TPSL1采用深度优先、从左到右的输入搜索策略,证明格上基于Horn子句集的定理;MTPSL_2分为两部分:①利用Chang的单位归结通用证明程序,证明格上基于Horn集的定理;②利用MOL—归结,并采用深度优先及删除与半最小文字的启发策略的通用证明程序,证明格上基于非Horn集的定理。同时,给出了有关算法的完备性定理与相容性定理。 In this paper, Robinson’s principle of reduction is used to implement the theorem proving systems on two lattices - Prolys and Lisp respectively - TPSL1 and MTPSL2. Among them, TPSL1 uses a depth-first, left-to-right input search strategy to prove that the lattice is based on the Horn clause set theorem; MTPSL_2 is divided into two parts: ①Using Chang’s unit to generalize the proof procedure, ; (2) a general proof procedure using MOL-summed-up and using the heuristic strategies of depth-first and delete and semi-minimal words to prove the theorem based on non-Horn sets. At the same time, the completeness theorem and compatibility theorem of the algorithm are given.