{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,4]],"date-time":"2025-09-04T13:24:24Z","timestamp":1756992264122},"reference-count":37,"publisher":"Elsevier BV","issue":"4","license":[{"start":{"date-parts":[[1971,10,1]],"date-time":"1971-10-01T00:00:00Z","timestamp":55123200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Information Sciences"],"published-print":{"date-parts":[[1971,10]]},"DOI":"10.1016\/s0020-0255(71)80013-0","type":"journal-article","created":{"date-parts":[[2005,7,2]],"date-time":"2005-07-02T14:48:06Z","timestamp":1120315686000},"page":"315-342","source":"Crossref","is-referenced-by-count":14,"title":["Finding resolution proofs and using duplicate goals in and\/or trees"],"prefix":"10.1016","volume":"3","author":[{"given":"James R.","family":"Slagle","sequence":"first","affiliation":[]},{"given":"Deena A.","family":"Koniver","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S0020-0255(71)80013-0_bib1","series-title":"Theoretical Approaches to Non-Numerical Problem Solving","first-page":"179","article-title":"On the representation of problems and goal-directed procedures for computers","author":"Amarel","year":"1970"},{"key":"10.1016\/S0020-0255(71)80013-0_bib2","doi-asserted-by":"crossref","unstructured":"George, W. Baylor, Herbert, A. Simon, Chess mating combinations program, Proc. AFIPS 1966 Spring Joint Computing Conference, 431\u2013447.","DOI":"10.1145\/1464182.1464233"},{"key":"10.1016\/S0020-0255(71)80013-0_bib3","article-title":"A Deductive Question-Answering System","author":"Black","year":"1964"},{"key":"10.1016\/S0020-0255(71)80013-0_bib4","first-page":"113","article-title":"Automatic theorem proving with equality substitutions and mathematical induction","volume":"3","author":"Darlington","year":"1968"},{"key":"10.1016\/S0020-0255(71)80013-0_bib5","article-title":"Generality and GPS","author":"Ernst","year":"1967"},{"key":"10.1016\/S0020-0255(71)80013-0_bib6","series-title":"Computers and Thought","year":"1963"},{"key":"10.1016\/S0020-0255(71)80013-0_bib7","series-title":"Proc. International Conference on Information Processing","article-title":"Realization of a geometry proving machine","author":"Gelernter","year":"1959"},{"key":"10.1016\/S0020-0255(71)80013-0_bib8","doi-asserted-by":"crossref","unstructured":"Herbert Gelernter, J.R. Hansen and D.W. Loveland, Empirical explorations of the geometry theorem machine, Proc. 1960 Western Joint Computer Conference, 143\u2013147 (reprinted in [6]).","DOI":"10.1145\/1460361.1460381"},{"key":"10.1016\/S0020-0255(71)80013-0_bib9","unstructured":"C. Green and Bertram Raphael, The use of theorem-proving techniques in questionanswering systems, Proc. 1968 ACM National Conference, 169\u2013181."},{"key":"10.1016\/S0020-0255(71)80013-0_bib10","article-title":"A Completeness Theorem and a Computer Program for Finding Theorems Derivable from Given Axioms","author":"Char-Tung Lee","year":"1967"},{"key":"10.1016\/S0020-0255(71)80013-0_bib11","author":"McCarthy","year":"1962"},{"key":"10.1016\/S0020-0255(71)80013-0_bib12","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","author":"Meltzer","year":"1966","journal-title":"Comput. J."},{"key":"10.1016\/S0020-0255(71)80013-0_bib13","series-title":"Self Organizing Systems","first-page":"153","article-title":"A variety of intelligent learning in a general problem solver","author":"Newell","year":"1960"},{"key":"10.1016\/S0020-0255(71)80013-0_bib14","series-title":"Self Organizing Systems 1962","first-page":"393","article-title":"Some problems of basic organization in problem solving programs","author":"Newell","year":"1962"},{"key":"10.1016\/S0020-0255(71)80013-0_bib15","series-title":"Proc. IFIP Congress","article-title":"Searching problem-solving and game-playing trees for minimal cost solutions","author":"Nilsson","year":"1968"},{"key":"10.1016\/S0020-0255(71)80013-0_bib16","article-title":"An Experience-Gathering Problem-Solving System","author":"Ross Quinlan","year":"1968"},{"key":"10.1016\/S0020-0255(71)80013-0_bib17","first-page":"135","article-title":"Parmodulation and theorem proving in first order theories with equality","volume":"4","author":"Robinson","year":"1969"},{"key":"10.1016\/S0020-0255(71)80013-0_bib18","article-title":"Some Theorem-Proving Strategies and Their Implementation","author":"Robinson","year":"1964"},{"key":"10.1016\/S0020-0255(71)80013-0_bib19","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","article-title":"A machine oriented logic based on the resolution principle","volume":"12","author":"Robinson","year":"1965","journal-title":"J. ACM"},{"key":"10.1016\/S0020-0255(71)80013-0_bib20","first-page":"227","article-title":"Automatic deduction with hyper-resolution","volume":"1","author":"Robinson","year":"1965","journal-title":"Intern. J. Comput. Math."},{"key":"10.1016\/S0020-0255(71)80013-0_bib21","article-title":"A review of automatic theorem proving","volume":"19","author":"Robinson","year":"1966"},{"key":"10.1016\/S0020-0255(71)80013-0_bib22","first-page":"2","article-title":"An overview of mechanical theorem proving","author":"Robinson","year":"1970"},{"key":"10.1016\/S0020-0255(71)80013-0_bib23","series-title":"Proc. International Joint Conference on Artificial Intelligence","article-title":"Concepts and methods for heuristic search","author":"Sandewall","year":"1969"},{"key":"10.1016\/S0020-0255(71)80013-0_bib24","doi-asserted-by":"crossref","first-page":"507","DOI":"10.1145\/321186.321193","article-title":"A heuristic program that solves symbolic integration problems in freshman calculus","volume":"10","author":"Slagle","year":"1963","journal-title":"J. ACM"},{"key":"10.1016\/S0020-0255(71)80013-0_bib25","series-title":"Proc. IFIP Congress","article-title":"A multipurpose theorem-proving, heuristic program that learns","author":"Slagle","year":"1965"},{"key":"10.1016\/S0020-0255(71)80013-0_bib26","doi-asserted-by":"crossref","first-page":"792","DOI":"10.1145\/365691.365960","article-title":"Experiments with a deductive question-answering program","volume":"8","author":"Slagle","year":"1965","journal-title":"Comm. ACM"},{"key":"10.1016\/S0020-0255(71)80013-0_bib27","doi-asserted-by":"crossref","first-page":"687","DOI":"10.1145\/321420.321428","article-title":"Automatic theorem proving with renamable and semantic resolution","volume":"14","author":"Slagle","year":"1967","journal-title":"J. ACM"},{"key":"10.1016\/S0020-0255(71)80013-0_bib28","series-title":"Theoretical Approaches to Non-numerical Problem Solving","first-page":"246","article-title":"Heuristic search programs","author":"Slagle","year":"1970"},{"key":"10.1016\/S0020-0255(71)80013-0_bib29","author":"Slagle","year":"1969"},{"key":"10.1016\/S0020-0255(71)80013-0_bib30","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1145\/321439.321444","article-title":"Experiments with a multipurpose, theorem-proving heuristic program","volume":"15","author":"Slagle","year":"1968","journal-title":"J. ACM"},{"key":"10.1016\/S0020-0255(71)80013-0_bib31","series-title":"Proc. International Joint Conference on Artificial Intelligence","article-title":"Completeness theorems for semantic resolution in consequence-finding","author":"Slagle","year":"1969"},{"key":"10.1016\/S0020-0255(71)80013-0_bib32","doi-asserted-by":"crossref","DOI":"10.1145\/362515.362560","article-title":"Experiments in automatic learning for a multipurpose heuristic program","volume":"14","author":"Slagle","year":"1971","journal-title":"Comm. ACM"},{"issue":"No. 7","key":"10.1016\/S0020-0255(71)80013-0_bib33","doi-asserted-by":"crossref","first-page":"727","DOI":"10.1287\/mnsc.11.7.727","article-title":"Assembly line balancing using probabilistic combinations of heuristics","volume":"11","author":"Tonge","year":"1965","journal-title":"Management Sci."},{"key":"10.1016\/S0020-0255(71)80013-0_bib34","series-title":"Proc. International Joint Conference on Artificial Intelligence","article-title":"PROW: A step toward automatic program writing","author":"Waldinger","year":"1969"},{"key":"10.1016\/S0020-0255(71)80013-0_bib35","author":"Wos","year":"1965","journal-title":"A catalogue of PG problems"},{"key":"10.1016\/S0020-0255(71)80013-0_bib36","doi-asserted-by":"crossref","unstructured":"L. Wos, D. Carson and G. Robinson, The unit preference strategy in theorem proving, Proc. 1964 Fall Joint Computer Conference, 616\u2013621.","DOI":"10.1145\/1464052.1464109"},{"key":"10.1016\/S0020-0255(71)80013-0_bib37","doi-asserted-by":"crossref","first-page":"536","DOI":"10.1145\/321296.321302","article-title":"The efficiency and completeness of the set of support strategy in theorem proving","volume":"12","author":"Wos","year":"1965","journal-title":"J. ACM"}],"container-title":["Information Sciences"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0020025571800130?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0020025571800130?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2023,5,3]],"date-time":"2023-05-03T17:10:46Z","timestamp":1683133846000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0020025571800130"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1971,10]]},"references-count":37,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1971,10]]}},"alternative-id":["S0020025571800130"],"URL":"https:\/\/doi.org\/10.1016\/s0020-0255(71)80013-0","relation":{},"ISSN":["0020-0255"],"issn-type":[{"value":"0020-0255","type":"print"}],"subject":[],"published":{"date-parts":[[1971,10]]}}}