{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:23:46Z","timestamp":1725456226523},"publisher-location":"Berlin\/Heidelberg","reference-count":15,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"354019343X"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0012864","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T01:12:39Z","timestamp":1132708359000},"page":"658-674","source":"Crossref","is-referenced-by-count":1,"title":["An implementation of a dissolution-based system employing theory links"],"prefix":"10.1007","author":[{"given":"Neil V.","family":"Murray","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Erik","family":"Rosenthal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"2","key":"45_CR1","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1145\/322248.322249","volume":"28","author":"P.B. Andrews","year":"1981","unstructured":"Andrews, P.B. Theorem proving via general matings. J.ACM 28,2 (April 1981), 193\u2013214.","journal-title":"J.ACM"},{"key":"45_CR2","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1016\/0304-3975(79)90054-9","volume":"8","author":"W. Bibel","year":"1979","unstructured":"Bibel, W. Tautology testing with a generalized matrix reduction method. Theoretical Computer Science 8 (1979) 31\u201344.","journal-title":"Theoretical Computer Science"},{"issue":"4","key":"45_CR3","doi-asserted-by":"publisher","first-page":"633","DOI":"10.1145\/6490.6491","volume":"33","author":"D. Champeaux de","year":"1986","unstructured":"de Champeaux, D. Sub-problem finder and instance checker, two cooperating modules for theorem provers. J.ACM 33,4 (1986), 633\u2013657.","journal-title":"J.ACM"},{"key":"45_CR4","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1016\/0304-3975(85)90144-6","volume":"39","author":"A. Haken","year":"1985","unstructured":"Haken, A. The intractability of resolution. Theoretical Computer Science, 39 (1985), 297\u2013308.","journal-title":"Theoretical Computer Science"},{"key":"45_CR5","doi-asserted-by":"crossref","unstructured":"Lusk, E., and Overbeek, R. A portable environment for research in automated reasoning. Proceedings of CADE-7, Napa, CA, May 14\u201316, 1984. In Lecture Notes in Computer Science, Springer-Verlag, Vol. 170, 43\u201352.","DOI":"10.1007\/BFb0047112"},{"issue":"2","key":"45_CR6","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1145\/23005.23716","volume":"34","author":"N.V. Murray","year":"1987","unstructured":"Murray, N.V., and Rosenthal, E. Inference with Path Resolution and Semantic Graphs. J.ACM 34,2 (April 1987), 225\u2013254.","journal-title":"J.ACM"},{"key":"45_CR7","unstructured":"Murray, N.V., and Rosenthal, E. Path dissolution: A strongly complete rule of inference. Proceedings of the 6 th National Conference on Artificial Intelligence, Seattle, WA, July 12\u201317, 1987, 161\u2013166."},{"key":"45_CR8","unstructured":"Murray, N.V., and Rosenthal, E. Inferencing on an arbitrary set of links. Proceedings of the 2 nd International Symposium on Methodologies for Intelligent Systems, Charlotte, NC, October 1987. In Methodologies for Intelligent Systems, (Ras, Z. and Zemankova, M., eds.) North-Holland, 1987, 416\u2013423."},{"key":"45_CR9","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/3-540-16780-3_102","volume-title":"8th International Conference on Automated Deduction","author":"Neil V. Murray","year":"1986","unstructured":"Murray, N.V., Rosenthal, E. Theory links in semantic graphs. Proceedings of the 8th International Conference on Automated Deduction, Oxford, England, July 1986. In Lecture Notes in Computer Science, Springer-Verlag, Vol. 230, 353\u2013364."},{"key":"45_CR10","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/BF02432151","volume":"2","author":"F.J. Pelletier","year":"1986","unstructured":"Pelletier, F.J. Seventy-Five Problems for Testing Automatic Theorem-Provers. Journal of Automated Reasoning 2 (1986) 191\u2013216.","journal-title":"Journal of Automated Reasoning"},{"key":"45_CR11","first-page":"227","volume":"1","author":"J.A. Robinson","year":"1965","unstructured":"Robinson, J.A. Automatic deduction with hyper-resolution. International Journal of Computer Mathematics, 1 (1965), 227\u2013234.","journal-title":"International Journal of Computer Mathematics"},{"issue":"4","key":"45_CR12","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/BF00244275","volume":"1","author":"M.E. Stickel","year":"1985","unstructured":"Stickel, M.E. Automated deduction by theory resolution. J. Automated Reasoning, 1,4 (1985), 333\u2013355.","journal-title":"J. Automated Reasoning"},{"key":"45_CR13","doi-asserted-by":"crossref","first-page":"573","DOI":"10.1007\/3-540-16780-3_122","volume-title":"8th International Conference on Automated Deduction","author":"Mark E. Stickel","year":"1986","unstructured":"Stickel, M.E. A Prolog technology theorem prover: implementation by an extended Prolog compiler. Proceedings of the 8 th International Conference on Automated Deduction, Oxford, England, July 1986. In Lecture Notes in Computer Science, Springer-Verlag, Vol. 230, 573\u2013587."},{"key":"45_CR14","unstructured":"Stickel, M.E. Personal Communication. November 1987."},{"key":"45_CR15","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1007\/978-1-4899-5327-8_25","volume-title":"Studies in Constructive Mathematics and Mathematical Logic Part 2","author":"G. S. Tseitin","year":"1970","unstructured":"Tseitin, G. S. On the complexity of derivations in propositional calculus. Structures in Constructive Mathematics and Mathematical Logic, Part II, A. O. Sliosenko, ed. (1968), 115\u2013125."}],"container-title":["Lecture Notes in Computer Science","9th International Conference on Automated Deduction"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/www.springerlink.com\/index\/pdf\/10.1007\/BFb0012864","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T00:24:44Z","timestamp":1586564684000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0012864"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354019343X"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/bfb0012864","relation":{},"subject":[]}}