### Automatic Theorem Proving With Renamable and Semantic ResolutionAutomatic Theorem Proving With Renamable and Semantic Resolution

Access Restriction
Subscribed

 Author Slagle, James R. Source ACM Digital Library Content type Text Publisher Association for Computing Machinery (ACM) File Format PDF Copyright Year ©1967 Language English
 Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science 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 $\textit{M},$ semantic resolution is the resolution of a latent clash in which each “electron” is at least sometimes false under $\textit{M};$ the nucleus is at least sometimes true under $\textit{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 $\textit{U}$ is a finite, truth-functionally unsatisfiable set of nonempty clauses and if $\textit{M}$ is a ground model, then there exists an unresolved maximal semantic clash $[\textit{E}1,$ $\textit{E}2,$ · · ·, $\textit{E}q,$ $\textit{C}]$ with nucleus $\textit{C}$ such that any set containing $\textit{C}$ and one or more of the electrons $\textit{E}1,$ $\textit{E}2,$ · · ·, $\textit{E}q$ is an unresolved semantic clash in $\textit{U}.$ ISSN 00045411 Age Range 18 to 22 years ♦ above 22 year Educational Use Research Education Level UG and PG Learning Resource Type Article Publisher Date 1967-10-01 Publisher Place New York e-ISSN 1557735X Journal Journal of the ACM (JACM) Volume Number 14 Issue Number 4 Page Count 11 Starting Page 687 Ending Page 697

#### Open content in new tab

Source: ACM Digital Library