Access Restriction

Author Andrews, Peter B.
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Copyright Year ©1968
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Abstract A refinement of the resolution method for mechanical theorem proving is presented. A resolvent $\textit{C}$ of clauses $\textit{A}$ and $\textit{B}$ is called a $\textit{merge}$ if literals from $\textit{A}$ and $\textit{B}$ merge together to form some literal of $\textit{C}.$ It is shown that the resolution method remains complete if it is required that two noninitial clauses which are not merges never be resolved with one another. It is also shown that this strategy can be combined with the set-of-support strategy.
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 1968-07-01
Publisher Place New York
e-ISSN 1557735X
Journal Journal of the ACM (JACM)
Volume Number 15
Issue Number 3
Page Count 15
Starting Page 367
Ending Page 381

Open content in new tab

   Open content in new tab
Source: ACM Digital Library