{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,4]],"date-time":"2022-04-04T23:16:50Z","timestamp":1649114210995},"reference-count":22,"publisher":"Association for Computing Machinery (ACM)","issue":"3","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[1970,7]]},"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\u00f6del'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.<\/jats:p>","DOI":"10.1145\/321592.321604","type":"journal-article","created":{"date-parts":[[2002,7,27]],"date-time":"2002-07-27T11:26:13Z","timestamp":1027769173000},"page":"535-542","source":"Crossref","is-referenced-by-count":17,"title":["Interpolation Theorems for Resolution in Lower Predicate Calculus"],"prefix":"10.1145","volume":"17","author":[{"given":"James R.","family":"Slagle","sequence":"first","affiliation":[{"name":"Department of Health, Education and Welfare, Division of Computer Research and Technology, National Institutes of HeMth, Public Health Service Bethesda, Maryland"}]}],"member":"320","reference":[{"key":"e_1_2_1_1_2","volume-title":"Koninkl. Ned. Akad. Wetcnsehap.","year":"1953"},{"key":"e_1_2_1_2_2","doi-asserted-by":"crossref","first-page":"250","DOI":"10.2307\/2963593","article-title":"Linear reasoning. A new form of the Herbrand-Gentzen theorem","volume":"22","year":"1957","journal-title":"J. Symbolic Logic"},{"key":"e_1_2_1_3_2","doi-asserted-by":"crossref","first-page":"269","DOI":"10.2307\/2963594","article-title":"Three uses of the Herbrand-Gentzen theorem relating model theorem to proof theorem","volume":"22","author":"CRAIG","year":"1957","journal-title":"J. Symbolic Logic"},{"key":"e_1_2_1_4_2","first-page":"113","volume-title":"Machine Intelligence","volume":"3","year":"1968"},{"key":"e_1_2_1_5_2","first-page":"349","article-title":"Die Vollstandigbert der Axiome des Logischen Vunktionen Kalkuls","volume":"87","year":"1930","journal-title":"Monatsh. Math. Phys."},{"key":"e_1_2_1_6_2","first-page":"169","volume-title":"Proc. 23rd Nat. Conf. ACM","year":"1968"},{"key":"e_1_2_1_7_2","unstructured":"com.atypon.pdfplus.internal.model.plusxml.impl.AuthorGroup@1baa72f7\n The arbitrarily-large entities in man-machine mathematics. In Formal Systems and Non-numerical Problem Solving by Computers Mesarovic Mihajlo D. and Banerji Ranan B. (Eds.) (in press). GUARD J. The arbitrarily-large entities in man-machine mathematics. In Formal Systems and Non-numerical Problem Solving by Computers Mesarovic Mihajlo D. and Banerji Ranan B. (Eds.) (in press)."},{"key":"e_1_2_1_8_2","unstructured":"com.atypon.pdfplus.internal.model.plusxml.impl.AuthorGroup@3738a9b5\n Ma~-hematical Logic. Wiley New York 1967. KLEENE STEPHEN COLE. Ma~-hematical Logic. Wiley New York 1967."},{"key":"e_1_2_1_9_2","volume-title":"Calif.","year":"1967"},{"key":"e_1_2_1_10_2","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1093\/comjnl\/8.4.341","article-title":"Theorem proving for computers: Some results on resolution and renaming","volume":"8","year":"1966","journal-title":"Computer J."},{"key":"e_1_2_1_11_2","first-page":"47","volume-title":"Koninkl. Ned. Akad. Wetenschap.","year":"1956"},{"key":"e_1_2_1_12_2","first-page":"135","volume-title":"Machine Intelligence","year":"1968"},{"key":"e_1_2_1_13_2","unstructured":"com.atypon.pdfplus.internal.model.plusxml.impl.AuthorGroup@4e2b3cdf\n A machine-oriented logic based on the resolution principle. J. ACM i~ 1 (Jan. 1965) 23-41. 10.1145\/321250.321253 ROBINSON J.A. A machine-oriented logic based on the resolution principle. J. ACM i~ 1 (Jan. 1965) 23-41. 10.1145\/321250.321253"},{"key":"e_1_2_1_14_2","first-page":"227","article-title":"deduction with hyper-resolution","year":"1965","journal-title":"Internat. J. of Computer Math."},{"key":"e_1_2_1_15_2","first-page":"1","volume-title":"Proc. Symposia in Appl. Math. (1966","volume":"19","year":"1967"},{"key":"e_1_2_1_16_2","unstructured":"Automatic \n Present state of mathematical theorem proving. In Formal Systems and Nonnumerical Problem Solving by Computers Mesarovic Mihajlo D. and Banerji Ranan B. (Eds.) (in press). --. Present state of mathematical theorem proving. In Formal Systems and Nonnumerical Problem Solving by Computers Mesarovic Mihajlo D. and Banerji Ranan B. (Eds.) (in press)."},{"key":"e_1_2_1_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/321420.321428"},{"key":"e_1_2_1_18_2","unstructured":"SLAGLE JAMES \n Heuristics search program. In Formal Systems and Non-numerical Problem Solving by Computers Mesarovic Mihajlo D. and Banerji Ranan B. (Eds.) (in press). --. Heuristics search program. In Formal Systems and Non-numerical Problem Solving by Computers Mesarovic Mihajlo D. and Banerji Ranan B. (Eds.) (in press)."},{"key":"e_1_2_1_19_2","volume-title":"Md.","year":"1969"},{"key":"e_1_2_1_20_2","volume-title":"Mass.","year":"1967"},{"key":"e_1_2_1_21_2","first-page":"615","volume-title":"Proc. AFIPS 1964 Fall Joint Comp. Conf.","volume":"26"},{"key":"e_1_2_1_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/321296.321302"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/321592.321604","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,3,2]],"date-time":"2021-03-02T17:55:06Z","timestamp":1614707706000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/321592.321604"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1970,7]]},"references-count":22,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1970,7]]}},"alternative-id":["10.1145\/321592.321604"],"URL":"http:\/\/dx.doi.org\/10.1145\/321592.321604","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":["Artificial Intelligence","Hardware and Architecture","Information Systems","Control and Systems Engineering","Software"],"published":{"date-parts":[[1970,7]]}}}