Proof Procedure based on Modified Analytic Tableaux
Hajime Sawamura, Takashi Maeda, Michiaki Kawaguchi · Hokkaido University Collection of Scholarly and Academic Papers (Hokkaido University) · 1976
A formal, mechanical approach to theorem-proving appears to be the most promising from a standpoint of realizing the need for inference in the field of deductive science.In this paper, we have described an effective and fiexible proof procedure in mechanical theorem-proving.The modified analytic tableaux is a variant of the "analytic tableaux" of Smullyan.This method is compatible with the resolution method, which forms the basis for probably all contemporary theoremprovers for predicate calculus, Theoretically, the proposed proof procedure can be considered as an extension of the resolution method.Also, it was proved that this proof procedure is complete, and several applications of this method are discussed.