A reduction method for theorem proving based on the partial-instantiation technique

摘要

Logical inference is of central importance in the information and decision science. First-order predicate inference (theorem proving) provides more powerful representation of models and of knowledge, but presents a hard computational problem. We extend Jeroslow's theorem-proving procedure in function-free formulas to be applicable to full first-order predicate formulas. Therefore, proposed theorem-proving procedure can be more flexible tool for data handling and inferences. Our proposed procedure is based on the partial-instantiation technique, which reduces a first-order predicate clausal-form formula to an incrementally augmented propositional formula and proves the theorem by checking the satisfiability of the propositional formula. We also show the completeness of the proposed procedure, i.e., it can detect the unsatisfiability of an input formula. Furthermore, we compare it with resolution-style theorem-proving program otter and show the efficiency of the proposed procedure.