Theorem proving based on the partial instantiation technique
Masahito Yamamoto, Azuma Ohuchi, Toshio Ohyanagi · Electronics and Communications in Japan (Part III Fundamental Electronic Science) · 1996
Abstract For studies toward the automated theorem proving, various methods and strategies have been presented based on the resolution principle proposed by Robinson in 1965. Most of the theorem‐proving systems at present are based on this resolution principle. In constrast to this, Jeroslow proposed the partial instantiation technique in 1988. the method proposed by Jeroslow, however, has a problem in that only the formula not containing function symbols is considered and the efficiency is low since the clause form is not assumed. the authors improved Jeroslow's method. A procedure was proposed where satisfiability is decided for the formula of the clause form not containing function sysmbols, and the effectiveness of the method is demonstrated. This paper extends the above procedure and proposes a theorem‐proving procedure so that the formula containing function symbols can be handled. A proof is given that the proposed procedure is complete. A comparison experiment is executed, and the effectiveness of the proposed procedure is investigated.