On constructing theorem prover based on resolution with Java

摘要

In order to construct theorem prover based on resolution with Java, we introduce two data structures called FVar/BVar and Termlist methods. Our experience shows that the Termust method runs faster than the FVar/BVar methods when unifying several terms except deep nested terms. We also implement a tentative theorem prover using both methods. The prover using Termlist can prove almost problems faster than that using FVar/BVar does.