REALIZATION OF THEOREM PROVING ON A MINI-COMPUTER
Xianchang Zeng · Chinese Journal of Computers · 1981
This paper describes the concrete process of using BASIC to realize theorem proving on a mini-computer PDP-11-03. The only rule of inference used is a refinement algorithm-the Unit Binary Eesolution. A few of technics as follows:1. The subsumption test. This technic can be used to delete some irrelevant and redundant clauses. With the Fast-Search-Method, some unnecessary teats can be avoided. For instance, let C1, C2, …, Cn be the given old unit clauses and D1, D2, …, Dm be the new ones. If D1, D2, …, Dm. do not subsume each other, m(m-1)/2 times of search can be saved.2. The test of the ordinal number of clauses. To resolve a unit clause, say clause m, against a nonunit clause, say clause n', we first find the last unit clause, say clause m', which is used to obtain clause n'. If m is less than m', we resolve clause m and clause n'; otherwise, they are not resolved. (Using it, we can avoid repeatedly generating the same unit clause.)3. The supporting set. The supporting set can be used to avoid performing any resolution in the basic axioms.4. The programming technic. The nest structure of ALGOL is introduced into BASIC programs so that only one-dimension string array and a few simple variables are needed. Chain structure is used to realize the exchange between the Polish notation and the usual notation of clauses. The dialogue between the user and computer can be used to speed up finding proofs of theorems.