{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,9]],"date-time":"2026-07-09T06:48:38Z","timestamp":1783579718836,"version":"3.55.0"},"reference-count":23,"publisher":"Elsevier BV","issue":"3-4","license":[{"start":{"date-parts":[[1971,12,1]],"date-time":"1971-12-01T00:00:00Z","timestamp":60393600000},"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":["Artificial Intelligence"],"published-print":{"date-parts":[[1971,12]]},"DOI":"10.1016\/0004-3702(71)90012-9","type":"journal-article","created":{"date-parts":[[2003,3,14]],"date-time":"2003-03-14T13:02:52Z","timestamp":1047646972000},"page":"227-260","source":"Crossref","is-referenced-by-count":232,"title":["Linear resolution with selection function"],"prefix":"10.1016","volume":"2","author":[{"given":"Robert","family":"Kowalski","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Donald","family":"Kuehner","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"78","reference":[{"key":"10.1016\/0004-3702(71)90012-9_BIB1","doi-asserted-by":"crossref","first-page":"525","DOI":"10.1145\/321592.321603","article-title":"A linear format for resolution with merging and a new technique for establishing completeness","volume":"17","author":"Anderson","year":"1970","journal-title":"J. ACM"},{"key":"10.1016\/0004-3702(71)90012-9_BIB2","doi-asserted-by":"crossref","first-page":"367","DOI":"10.1145\/321466.321469","article-title":"Resolution with merging","volume":"15","author":"Andrews","year":"1968","journal-title":"J. ACM"},{"key":"10.1016\/0004-3702(71)90012-9_BIB3","doi-asserted-by":"crossref","DOI":"10.1109\/TSSC.1968.300136","article-title":"A formal basis for the heuristic determination of minimum cost paths","author":"Hart","year":"1968","journal-title":"I.E.E.E. Transactions on System Sciences and Cybernetics"},{"key":"10.1016\/0004-3702(71)90012-9_BIB4","first-page":"87","article-title":"Semantic trees in automatic theorem proving","volume":"4","author":"Hayes","year":"1969"},{"key":"10.1016\/0004-3702(71)90012-9_BIB5","article-title":"Lecture notes on automatic theorem-proving","volume":"40","author":"Hayes","year":"1971"},{"key":"10.1016\/0004-3702(71)90012-9_BIB6","author":"Kieburtz","year":"1969","journal-title":"Compatibility of Refinements of the Resolution Principle"},{"key":"10.1016\/0004-3702(71)90012-9_BIB7","first-page":"181","article-title":"Search strategies for theorem-proving","volume":"5","author":"Kowalski","year":"1970"},{"key":"10.1016\/0004-3702(71)90012-9_BIB8","article-title":"Studies in the completeness and efficiency of theorem-proving by resolution","author":"Kowalski","year":"1970"},{"key":"10.1016\/0004-3702(71)90012-9_BIB9","first-page":"73","article-title":"A note on the relation between resolution and Maslov's inverse method","volume":"6","author":"Kuehner","year":"1971"},{"key":"10.1016\/0004-3702(71)90012-9_BIB10","article-title":"Strategies for improving the efficiency of automatic theorem-proving","author":"Kuehner","year":"1971"},{"key":"10.1016\/0004-3702(71)90012-9_BIB11","article-title":"Linear resolution with selection function","author":"Kowalski","year":"1970"},{"key":"10.1016\/0004-3702(71)90012-9_BIB12","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1145\/321526.321527","article-title":"A simplified format for the model-elimination theorem-proving procedure","volume":"16","author":"Loveland","year":"1969","journal-title":"J. ACM"},{"key":"10.1016\/0004-3702(71)90012-9_BIB13","first-page":"147","article-title":"A linear format for resolution","volume":"125","author":"Loveland","year":"1970"},{"key":"10.1016\/0004-3702(71)90012-9_BIB14","series-title":"Some linear Herbrand proof procedures: an analysis","author":"Loveland","year":"1970"},{"key":"10.1016\/0004-3702(71)90012-9_BIB15","first-page":"163","article-title":"Refinement theorems in resolution theory","volume":"125","author":"Luckham","year":"1970"},{"key":"10.1016\/0004-3702(71)90012-9_BIB16","first-page":"77","article-title":"Proof-search strategies for methods of the resolution type","volume":"4","author":"Maslov","year":"1971"},{"key":"10.1016\/0004-3702(71)90012-9_BIB17","series-title":"Proceedings of the NATO Advanced Study Institute on Artificial Intelligence and Heuristic Programming","first-page":"15","article-title":"Prolegomena to a theory of efficiency of proof procedures","author":"Meltzer","year":"1971"},{"key":"10.1016\/0004-3702(71)90012-9_BIB18","first-page":"59","article-title":"Advances and problems in mechanical proof procedures","volume":"4","author":"Prawitz","year":"1969"},{"key":"10.1016\/0004-3702(71)90012-9_BIB19","series-title":"Two results on ordering for resolution with merging and linear format","author":"Reiter","year":"1970"},{"key":"10.1016\/0004-3702(71)90012-9_BIB20","first-page":"1","article-title":"A review of automatic theorem-proving","volume":"19","author":"Robinson","year":"1967"},{"key":"10.1016\/0004-3702(71)90012-9_BIB21","doi-asserted-by":"crossref","first-page":"687","DOI":"10.1145\/321296.321302","article-title":"Efficiency and completeness of the set of support strategy in theorem-proving","volume":"12","author":"Wos","year":"1965","journal-title":"J. ACM"},{"key":"10.1016\/0004-3702(71)90012-9_BIB22","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1016\/0004-3702(70)90011-1","article-title":"Resolution Graphs","volume":"1","author":"Yates","year":"1970","journal-title":"Artificial Intelligence"},{"key":"10.1016\/0004-3702(71)90012-9_BIB23","first-page":"54","article-title":"On a class of strategies which can be used to established decidability by the resolution principle","volume":"III","author":"Zamov","year":"1969"}],"container-title":["Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0004370271900129?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0004370271900129?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,3,26]],"date-time":"2019-03-26T23:23:31Z","timestamp":1553642611000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/0004370271900129"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1971,12]]},"references-count":23,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[1971,12]]}},"alternative-id":["0004370271900129"],"URL":"https:\/\/doi.org\/10.1016\/0004-3702(71)90012-9","relation":{},"ISSN":["0004-3702"],"issn-type":[{"value":"0004-3702","type":"print"}],"subject":[],"published":{"date-parts":[[1971,12]]}}}