Thumbnail
Access Restriction
Subscribed

Author Peterson, G. E.
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Copyright Year ©1976
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Abstract The concern here is with proof procedures which are generalizations of input or unit deduction. The author's generalizations of input deduction involve lemmas, whereas those of unit deduction involve longer clauses and are akin to Robinson's P1 deduction. Chang's theorem, which establishes the equivalence of input and unit refutation, is extended to these generalizations. Completeness results of Henschen, Wos, and Kuehner for input or unit deduction applied to Horn sets are generalized to apply also to non-Horn sets. A key result is that any unsatisfiable set can be refuted by a lock linear resolution procedure in which the only lemmas are positive clauses composed entirely of instances of a small set of literals which can be specified in advance. In an implementation such lemmas would be generated only infrequently, thus allowing one to periodically gather the lemmas, discard other generated clauses, and restart the proof procedure.
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 1976-10-01
Publisher Place New York
e-ISSN 1557735X
Journal Journal of the ACM (JACM)
Volume Number 23
Issue Number 4
Page Count 9
Starting Page 573
Ending Page 581


Open content in new tab

   Open content in new tab
Source: ACM Digital Library