Access Restriction

Author Slagle, James R.
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 The resolution principle is an inference rule for quantifier-free first-order predicate calculus. In the past, the completeness theorems for resolution and its refinements have been stated and proved for finite sets of clauses. It is easy (by Gödel's Compactness Theorem) and of practical interest to extend them to countable sets, thus allowing schemata representing denumerably many axioms. In addition, some theorems similar to Craig's Interpolation Theorem are proved for deduction by resolution. In propositional calculus, the theorem proved is stronger, whereas in predicate calculus the theorems proved are in some ways stronger and in some ways weaker than Craig's theorem. These interpolation theorems suggest procedures which could be embodied in computer programs for automatic proof finding and consequence finding.
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 8
Starting Page 535
Ending Page 542

Open content in new tab

   Open content in new tab
Source: ACM Digital Library