{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,19]],"date-time":"2025-09-19T08:47:45Z","timestamp":1758271665313},"reference-count":42,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"8","license":[{"start":{"date-parts":[[1976,8,1]],"date-time":"1976-08-01T00:00:00Z","timestamp":207705600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Comput."],"published-print":{"date-parts":[[1976,8]]},"DOI":"10.1109\/tc.1976.1674697","type":"journal-article","created":{"date-parts":[[2007,9,4]],"date-time":"2007-09-04T20:35:10Z","timestamp":1188938110000},"page":"782-801","source":"Crossref","is-referenced-by-count":30,"title":["Resolution, Refinements, and Search Strategies: A Comparative Study"],"prefix":"10.1109","volume":"C-25","author":[{"family":"Wilson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"family":"Minker","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref39","article-title":"an approach to parrallel inferences and parallel search","author":"wilson","year":"1975","journal-title":"IEEE Workshop on Automated Theorem Proving"},{"key":"ref38","first-page":"1171","article-title":"from planner to connivera genetic approach","volume":"41","author":"sussman","year":"1972","journal-title":"1972 Fall Joint Comput Conf Proc"},{"key":"ref33","author":"rulifson","year":"1972","journal-title":"Artificial Intelligence Center"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"},{"key":"ref31","author":"reboh","year":"1972","journal-title":"Study of automatic theorem-proving programs"},{"key":"ref30","author":"nilsson","year":"1971","journal-title":"Problem-Solving Methods in Artificial Intelligence"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1145\/321784.321792"},{"key":"ref36","author":"stickel","year":"1974","journal-title":"The programmable strategy theorem prover An implementation of the linear MESON procedure"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1145\/321420.321428"},{"key":"ref34","author":"siegel","year":"1956","journal-title":"Nonparametric Statistics for the Behavioral Sciences"},{"key":"ref10","author":"fishman","year":"1973","journal-title":"Experiments with resolution-based decuctive question?answering system and a proposes clause representation for parallel search"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1145\/321296.321302"},{"key":"ref11","first-page":"124","volume":"21","author":"fleisig","year":"1974","journal-title":"Courant Inst Math Sciences"},{"key":"ref12","first-page":"107","author":"glasner","year":"1964","journal-title":"The NUSPEAK systems"},{"key":"ref13","first-page":"167","article-title":"procedural embedding of knowledge of planner","author":"hewitt","year":"1971","journal-title":"Proc IJCAI (British Comput Soc"},{"key":"ref14","author":"kieburtz","year":"1970","journal-title":"Compatible strategies for the resolution principle"},{"key":"ref15","first-page":"87","volume":"4","author":"kowalski","year":"1969","journal-title":"Machine Intelligence"},{"key":"ref16","author":"kowalski","year":"0","journal-title":"Studies in the completeness and efficiency of theorem-proving by resolution"},{"key":"ref17","first-page":"181","volume":"5","author":"kowalski","year":"1970","journal-title":"Machine Intelligence"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(71)90012-9"},{"key":"ref19","author":"lawrence","year":"1974","journal-title":"Experimental tests of resolution based theorem-proving strategies"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(73)90013-1"},{"key":"ref4","author":"boyer","year":"0","journal-title":"The sharing of structure in resolution programs"},{"key":"ref27","first-page":"141","volume":"7","author":"michie","year":"1972","journal-title":"Machine Intelligence"},{"key":"ref3","year":"1973","journal-title":"UCI Lisp Manual"},{"key":"ref6","author":"bradley","year":"1968","journal-title":"Distribution-free statistical tests"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1007\/BF00976637"},{"key":"ref5","first-page":"101","volume":"7","author":"boyer","year":"1972","journal-title":"Machine Intelligence"},{"key":"ref8","first-page":"173","volume":"4","author":"darlington","year":"1969","journal-title":"Machine Intelligence"},{"key":"ref7","author":"burstall","year":"1971","journal-title":"Programming in POP-2"},{"key":"ref2","author":"aubin","year":"1974","journal-title":"Some experimental results on SL-resolution"},{"key":"ref9","first-page":"1193","article-title":"recent developments in sailan algol based language for artificial intelligence","volume":"41","author":"feldman","year":"1972","journal-title":"1972 Fall Joint Comput Conf Proc"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1145\/321466.321469"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1976.1674614"},{"key":"ref22","author":"luckham","year":"1968","journal-title":"The ancestry-filter method in automatic demonstration"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1145\/321694.321706"},{"key":"ref42","year":"0"},{"key":"ref24","article-title":"the use of user-supplied semantic information in resolution-based qa systems","author":"mcskimin","year":"1975","journal-title":"IEEE Workshop on Automatic Theorem Proving"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1145\/321420.321429"},{"key":"ref23","year":"1974","journal-title":"MRPPS 2 0 User's Manual"},{"key":"ref26","first-page":"15","author":"meltzer","year":"1971","journal-title":"Artificial Intelligence and Heuristic Programming"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/8.4.341"}],"container-title":["IEEE Transactions on Computers"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/12\/35150\/01674697.pdf?arnumber=1674697","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,29]],"date-time":"2021-11-29T20:39:26Z","timestamp":1638218366000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1674697\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1976,8]]},"references-count":42,"journal-issue":{"issue":"8"},"URL":"https:\/\/doi.org\/10.1109\/tc.1976.1674697","relation":{},"ISSN":["0018-9340"],"issn-type":[{"value":"0018-9340","type":"print"}],"subject":[],"published":{"date-parts":[[1976,8]]}}}