{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,11,21]],"date-time":"2023-11-21T05:35:40Z","timestamp":1700544940217},"reference-count":20,"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.1674701","type":"journal-article","created":{"date-parts":[[2007,9,4]],"date-time":"2007-09-04T16:35:10Z","timestamp":1188923710000},"page":"823-835","source":"Crossref","is-referenced-by-count":43,"title":["A Search Technique for Clause Interconnectivity Graphs"],"prefix":"10.1109","volume":"C-25","author":[{"family":"Sickel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref10","author":"michie","year":"1972","journal-title":"Machine Intelligence 7"},{"key":"ref11","author":"reboh","year":"1972","journal-title":"Study of automatic theorem-proving programs"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1145\/321662.321678"},{"key":"ref13","article-title":"fast unification","author":"robinson","year":"1976","journal-title":"Automatic Theorem Proving Workshop"},{"key":"ref14","author":"shostak","year":"1974","journal-title":"Refutation graphs and resolution theorem proving"},{"key":"ref15","author":"sickel","year":"1973","journal-title":"Extensions and comparisons of refinement strategies for theorem proving and applications in a parallel environment"},{"key":"ref16","author":"sickel","year":"1976","journal-title":"A proof description language for first-order predicate calculus"},{"key":"ref17","author":"sickel","year":"1975","journal-title":"A theorem prover based on clause interconnectivity graphs written in Algol W"},{"key":"ref18","author":"stickel","year":"1974","journal-title":"The programmable strategy theorem prover An implementation of the linear MESON procedure"},{"key":"ref19","author":"van vaalen","year":"1974","journal-title":"An extension of unification to substitution with an application to automatic theorem proving"},{"key":"ref4","author":"hopcroft","year":"1969","journal-title":"Formal Languages and Their Relation to Automata"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1145\/321796.321807"},{"key":"ref6","first-page":"316","volume":"i","author":"knuth","year":"1969","journal-title":"The art of computer programming"},{"key":"ref5","article-title":"algebraic aspects of unification","author":"huet","year":"1976","journal-title":"Automatic Theorem Proving Workshop"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1145\/321906.321919"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(71)90012-9"},{"key":"ref2","author":"andrews","year":"1975","journal-title":"Refutations by matings"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1145\/321592.321603"},{"key":"ref9","author":"mendelson","year":"1964","journal-title":"Introduction to Mathematical Logic"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(70)90011-1"}],"container-title":["IEEE Transactions on Computers"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/12\/35150\/01674701.pdf?arnumber=1674701","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,29]],"date-time":"2021-11-29T15:39:26Z","timestamp":1638200366000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1674701\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1976,8]]},"references-count":20,"journal-issue":{"issue":"8"},"URL":"https:\/\/doi.org\/10.1109\/tc.1976.1674701","relation":{},"ISSN":["0018-9340"],"issn-type":[{"value":"0018-9340","type":"print"}],"subject":[],"published":{"date-parts":[[1976,8]]}}}