Thumbnail
Access Restriction
Subscribed

Author Anderson, Robert ♦ Bledsoe, W. W.
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Copyright Year ©1970
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Abstract A new technique is given for establishing the completeness of resolution-based deductive systems for first-order logic (with or without equality) and several new completeness results are proved using this technique. The technique leads to very simple and clear completeness proofs and can be used to establish the completeness of most resolution-based deductive systems reported in the literature. The main new result obtained by means of this technique is that a linear format for resolution with merging and set of support and with several further restrictions is a complete deductive system for the first-order predicate calculus.
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 1970-07-01
Publisher Place New York
e-ISSN 1557735X
Journal Journal of the ACM (JACM)
Volume Number 17
Issue Number 3
Page Count 10
Starting Page 525
Ending Page 534


Open content in new tab

   Open content in new tab
Source: ACM Digital Library