Model generation theorem prover in KL1 using a ramified-stack algorithm

This paper presents a model-generation based parallel theorem prover for first-order logic implemented in KL1. The prover, called MGTP, is efficient in solving range-restricted non-Horn problems. The range-restrictedness condition allows us to represent object-level variables with KL1 variables, and to use only matching rather than full unification, thereby obtaining an interpreter that is very simple yet efficient. The implementation techniques developed are also useful for other related areas, such as truth maintenance systems and intelligent database systems. To improve the efficiency of MGTP, we also developed a ramified-stack (RAMS) algorithm for removing redundant computation during the conjunctive matching phase of a proving process. Experimental results show that an MGTP prover with RAMS can attain orders of magnitude of speedup over the naive one without RAMS, and can achieve good performance for non-Horn problems on a non-shared memory multiprocessor, Multi-PSI.