Thumbnail
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

   Open content in new tab
Source: ACM Digital Library