| The Great Theorem Prover (TGTP) based on the resolution refutation method for first-order logic has been developed and extended. The new version, TGTP(Z), improves the usage of unit clauses in searching for a unit refutation. In this thesis, we first analyzed how a hash technique was used for a refutation discovery in TGTP. Then a simplified unification was introduced to perform complementary matchings on unit clauses in order to obtain a unit refutation. TGTP(Z) was implemented with a combination of this unification and the hash technique which could be employed to delete identical copies of unit clauses. TGTP(Z) was tested on Stickle's problem set and showed the most powerful performance when compared with three other provers: TGTP (Newb91), PTTP (Stic88) and SETHEO (Letz92). Not only does it have the advantage of reducing the search overhead and the length of the proofs for many theorems in this set, but it is also faster and can solve all the problems in the set. Further improvements and possible applications of TGTP(Z) are also discussed in this manuscript. |
