Automatic Theorem Proving With Renamable and Semantic Resolution

TLDR

Semantic resolution resolves latent clashes where each electron is sometimes false and the nucleus sometimes true under a model, and its completeness follows from a general theorem about unsatisfiable clause sets. The authors unify and extend Robinson’s resolution theory and propose a theorem‑proving program based on semantic resolution, comparing it to hyper‑resolution and set‑of‑support resolution. They implement a semantic resolution theorem‑proving program and benchmark it against hyper‑resolution and set‑of‑support resolution. Renamable resolution is shown to be identical to 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 [ E 1 , E 2 , · · ·, E q , C ] with nucleus C such that any set containing C and one or more of the electrons E 1 , E 2 , · · ·, E q is an unresolved semantic clash in U .