{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T06:05:22Z","timestamp":1747548322694},"reference-count":29,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[1979,8,1]],"date-time":"1979-08-01T00:00:00Z","timestamp":302313600000},"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":[[1979,8]]},"DOI":"10.1016\/0004-3702(79)90015-8","type":"journal-article","created":{"date-parts":[[2003,3,14]],"date-time":"2003-03-14T13:02:52Z","timestamp":1047646972000},"page":"159-178","source":"Crossref","is-referenced-by-count":23,"title":["Using rewriting rules for connection graphs to prove theorems"],"prefix":"10.1016","volume":"12","author":[{"given":"C.L.","family":"Chang","sequence":"first","affiliation":[]},{"given":"J.R.","family":"Slagle","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/0004-3702(79)90015-8_BIB1","doi-asserted-by":"crossref","first-page":"801","DOI":"10.1109\/TC.1976.1674698","article-title":"Refutations by matings","author":"Andrews","year":"1976","journal-title":"IEEE Transactions on Computers C-25"},{"key":"10.1016\/0004-3702(79)90015-8_BIB2","series-title":"An efficient unification algorithm","author":"Baxter","year":"1973"},{"key":"10.1016\/0004-3702(79)90015-8_BIB3","series-title":"Theorem proving by generation of peudosemantic trees","author":"Chang","year":"1971"},{"key":"10.1016\/0004-3702(79)90015-8_BIB4","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1016\/S0020-0255(72)80012-4","article-title":"Theorem proving with variable-constrained resolution","volume":"4","author":"Chang","year":"1972","journal-title":"Information Sci."},{"key":"10.1016\/0004-3702(79)90015-8_BIB5","series-title":"Symbolic Logic and Mechanical Theorem Proving","author":"Chang","year":"1973"},{"key":"10.1016\/0004-3702(79)90015-8_BIB6","series-title":"Pattern Recognition and Artificial Intelligence","article-title":"deduce\u2014A deductive query language for relational data bases","author":"Chang","year":"1976"},{"key":"10.1016\/0004-3702(79)90015-8_BIB7","article-title":"deduce 2\u2014Further investigations of deduction in relational data bases","author":"Chang","year":"1978","journal-title":"IBM Research Report RJ2147"},{"key":"10.1016\/0004-3702(79)90015-8_BIB8","series-title":"Theorem proving by matching","author":"Chinlund","year":"1964"},{"key":"10.1016\/0004-3702(79)90015-8_BIB9","first-page":"15","article-title":"Eliminating the irrelevant from mechanical proofs","volume":"15","author":"Davis","year":"1963"},{"key":"10.1016\/0004-3702(79)90015-8_BIB10","series-title":"Proc. 5th International Joint Conference on Artificial Intelligence","article-title":"Theorem proving by covering expressions","author":"Henschen","year":"1977"},{"key":"10.1016\/0004-3702(79)90015-8_BIB11","series-title":"Presented at Automatic Theorem Proving Workshop","article-title":"Algebraic aspects of unification","author":"Huet","year":"1976"},{"key":"10.1016\/0004-3702(79)90015-8_BIB12","series-title":"Pattern-Directed Inference Systems","article-title":"Planning techniques for rule selection in deductive question-answering","author":"Klahr","year":"1977"},{"issue":"4","key":"10.1016\/0004-3702(79)90015-8_BIB13","doi-asserted-by":"crossref","first-page":"572","DOI":"10.1145\/321906.321919","article-title":"A proof procedure using connection graphs","volume":"22","author":"Kowalski","year":"1975","journal-title":"JACM"},{"key":"10.1016\/0004-3702(79)90015-8_BIB14","series-title":"Unification in linear time and space: A structured presentation","author":"Martelli","year":"1976"},{"key":"10.1016\/0004-3702(79)90015-8_BIB15","series-title":"Theorem proving with structure sharing and efficient unification","author":"Martelli","year":"1977"},{"key":"10.1016\/0004-3702(79)90015-8_BIB16","series-title":"Technical Note 148","article-title":"A production system for automatic deduction","author":"Nilsson","year":"1977"},{"key":"10.1016\/0004-3702(79)90015-8_BIB17","unstructured":"Nilsson, N.J. (1978): Private communications."},{"key":"10.1016\/0004-3702(79)90015-8_BIB18","series-title":"Linear Unification, RC5904 (#25518)","author":"Patterson","year":"1976"},{"key":"10.1016\/0004-3702(79)90015-8_BIB19","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1111\/j.1755-2567.1960.tb00558.x","article-title":"An improved proof procedure","volume":"26","author":"Prawitz","year":"1960","journal-title":"Theoria"},{"key":"10.1016\/0004-3702(79)90015-8_BIB20","first-page":"59","article-title":"Advances and problems in mechanical proof procedures","volume":"4","author":"Prawitz","year":"1969"},{"issue":"1","key":"10.1016\/0004-3702(79)90015-8_BIB21","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":"JACM"},{"key":"10.1016\/0004-3702(79)90015-8_BIB22","first-page":"63","article-title":"Computational logic: the unification computation","volume":"6","author":"Robinson","year":"1971"},{"key":"10.1016\/0004-3702(79)90015-8_BIB23","series-title":"Presented at Automatic Theorem Proving Workshop","article-title":"Fast unification","author":"Robinson","year":"1976"},{"key":"10.1016\/0004-3702(79)90015-8_BIB24","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1016\/0004-3702(76)90021-7","article-title":"Refutation graphs","volume":"7","author":"Shostak","year":"1976","journal-title":"Artificial Intelligence"},{"key":"10.1016\/0004-3702(79)90015-8_BIB25","doi-asserted-by":"crossref","first-page":"823","DOI":"10.1109\/TC.1976.1674701","article-title":"A search technique for clause interconnectivity graphs","author":"Sickel","year":"1976","journal-title":"IEEE Transactions on Computers C-25"},{"key":"10.1016\/0004-3702(79)90015-8_BIB26","series-title":"Proc. of IJCAI-77","first-page":"544","article-title":"Formal grammars as models of logic derivations","author":"Sickel","year":"1977"},{"key":"10.1016\/0004-3702(79)90015-8_BIB27","series-title":"Proc. ACM Symp. on Artificial Intelligence and Programming","first-page":"109","article-title":"prolog: The language and its implementation compared with lisp","author":"Warren","year":"1977"},{"key":"10.1016\/0004-3702(79)90015-8_BIB28","series-title":"IMM 412","article-title":"The linear conjuct and other algorithms for mechanical theorem proving","author":"Yarmush","year":"1976"},{"issue":"4","key":"10.1016\/0004-3702(79)90015-8_BIB29","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"}],"container-title":["Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0004370279900158?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0004370279900158?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:26:29Z","timestamp":1553642789000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/0004370279900158"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1979,8]]},"references-count":29,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1979,8]]}},"alternative-id":["0004370279900158"],"URL":"https:\/\/doi.org\/10.1016\/0004-3702(79)90015-8","relation":{},"ISSN":["0004-3702"],"issn-type":[{"value":"0004-3702","type":"print"}],"subject":[],"published":{"date-parts":[[1979,8]]}}}