Automatic Theorem Proving With Renamable and Semantic Resolution

Abstract

The theory of J. A. Robinson's resolution principle, an inference rule for first-order predicate calculus, is unified and extended. A theorem-proving computer program based on the new theory is proposed and the proposed semantic resolution program is compared with hyper-resolution and set-of-support resolution programs. Renamable and semantic resolution are defined and shown to be identical. Given a model M, semantic resolution is the resolution of a latent clash in which each 舠electron舡 is at least sometimes false under M; the nucleus is at least sometimes true under M.The completeness theorem for semantic resolution and all previous completeness theorems for resolution (including ordinary, hyper-, and set-of-support resolution) can be derived from a slightly more general form of the following theorem. If U is a finite, truth-functionally unsatisfiable set of nonempty clauses and if M is a ground model, then there exists an unresolved maximal semantic clash [E1, E2, ƃ ƃ ƃ, Eq, C] with nucleus C such that any set containing C and one or more of the electrons E1, E2, ƃ ƃ ƃ, Eq is an unresolved semantic clash in U. © 1967, ACM. All rights reserved.