{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:37:16Z","timestamp":1725493036269},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540422549"},{"type":"electronic","value":"9783540457442"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45744-5_14","type":"book-chapter","created":{"date-parts":[[2007,10,26]],"date-time":"2007-10-26T17:02:07Z","timestamp":1193418127000},"page":"182-194","source":"Crossref","is-referenced-by-count":2,"title":["Ordered Resolution vs. Connection Graph resolution"],"prefix":"10.1007","author":[{"given":"Reiner","family":"H\u00e4hnle","sequence":"first","affiliation":[]},{"given":"Neil V.","family":"Murray","sequence":"additional","affiliation":[]},{"given":"Erik","family":"Rosenthal","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,6,8]]},"reference":[{"issue":"3","key":"14_CR1","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1093\/logcom\/4.3.217","volume":"4","author":"L. Bachmair","year":"1994","unstructured":"Bachmair, L. and Ganzinger, H. Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation, 4(3):217\u2013247, 1994.","journal-title":"Journal of Logic and Computation"},{"key":"14_CR2","unstructured":"Beckert, B. and H\u00e4hnle, R. Analytic tableaux. In W. Bibel and P. Schmitt, editors, Automated Deduction: A Basis for Applications, volume I, chapter 1, pp. 11\u201341. Kluwer, 1998."},{"key":"14_CR3","doi-asserted-by":"publisher","first-page":"633","DOI":"10.1145\/322276.322277","volume":"28","author":"W. Bibel","year":"1981","unstructured":"Bibel, W. On matrics with connections. JACM, 28:633\u2013645, 1981.","journal-title":"JACM"},{"issue":"2","key":"14_CR4","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1145\/256303.256313","volume":"44","author":"W. Bibel","year":"1997","unstructured":"Bibel, W. and Eder, E. Decomposition of tautologies into regular formulas and strong completeness of connection graph resolution. Journal of the ACM, 44(2): 320\u2013344, 1997.","journal-title":"Journal of the ACM"},{"key":"14_CR5","unstructured":"de Nivelle, Hans. Ordering Refinements of Resolution. Ph.D. Thesis, Technische Universiteit Delft."},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"Dershowitz, N. Termination of rewriting. In J.-P. Jouannaud, editor, Rewriting Techniques and Applications, pages 69\u2013115. Academic Press, 1987. Reprinted from Journal of Symbolic Computation.","DOI":"10.1016\/S0747-7171(87)80022-6"},{"key":"14_CR7","unstructured":"Eisinger, N. Completeness, confluence, and related properties of clause graph resolution. Research notes in artificial intelligence. Pitman Publishing, 1991."},{"issue":"1","key":"14_CR8","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1145\/321958.321960","volume":"23","author":"W.H. Joyner","year":"1976","unstructured":"Joyner, W.H. Resolution strategies as decision procedures. J. ACM 23,1 (July 1976), 398\u2013417.","journal-title":"J. ACM"},{"key":"14_CR9","first-page":"87","volume":"4","author":"R. Kowalski","year":"1969","unstructured":"Kowalski, R. and Hayes, P.J. Semantic trees in automatic theorem proving. In Machine Intelligence, volume 4, pages 87\u2013101. Edinburgh University Press, 1969. Reprinted in [17].","journal-title":"Machine Intelligence"},{"issue":"4","key":"14_CR10","doi-asserted-by":"publisher","first-page":"572","DOI":"10.1145\/321906.321919","volume":"22","author":"R. Kowalski","year":"1975","unstructured":"Kowalski, R. A proof procedure using connection graphs. Journal of the ACM, 22(4):572\u2013595, 1975.","journal-title":"Journal of the ACM"},{"key":"14_CR11","unstructured":"Loveland, D.W., Automated Theorem Proving: A Logical Basis, North-Holland, New York (1978)."},{"issue":"3","key":"14_CR12","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1145\/174130.174135","volume":"40","author":"N.V. Murray","year":"1993","unstructured":"Murray, N.V. and Rosenthal, E. Dissolution: Making paths vanish. Journal of the ACM, 40(3):504\u2013535, 1993.","journal-title":"Journal of the ACM"},{"key":"14_CR13","volume-title":"Unpublished seminar notes","author":"J. Reynolds","year":"1966","unstructured":"Reynolds, J. Unpublished seminar notes, Stanford University, Palo Alto, CA, 1966."},{"key":"14_CR14","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"},{"key":"14_CR15","first-page":"103","volume-title":"Machine Intelligence 4","author":"E.E. Sibert","year":"1969","unstructured":"Sibert, E.E., A machine-oriented logic incorporating the equality relation, Machine Intelligence 4 (Meltzer and Michie, eds.), Edinburgh University Press, Edinburgh, 1969, 103\u2013133."},{"key":"14_CR16","volume-title":"Interner Bericht 7\/76, Institut","author":"J. Siekmann","year":"1976","unstructured":"Siekmann, J. and Stephan, W. Completeness and soundness of the connection graph procedure. Interner Bericht 7\/76, Institut I, Fakult\u00e4t f\u00fcr Informatik, Universit\u00fct Karlsruhe, 1976."},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"Siekmann, J. and Wrightson, G., editors.Automation of Reasoning: Classical Papers in Computational Logic 1967\u20131970, volume 2. Springer-Verlag, 1983.","DOI":"10.1007\/978-3-642-81952-0"},{"key":"14_CR18","doi-asserted-by":"crossref","unstructured":"Siekmann, J. and Wrightson, G., editors. Automation of Reasoning: Classical Papers in Computational Logic 1957\u20131966, volume 1. Springer-Verlag, 1983.","DOI":"10.1007\/978-3-642-81952-0"},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"Siekmann, J. and Wrightson, G. Erratum: a counterexample to W. Bibel\u2019s and E. Eder\u2019s strong completeness results for connection graph resolution. Journal of the ACM, to appear.","DOI":"10.1145\/363647.363697"},{"key":"14_CR20","doi-asserted-by":"crossref","unstructured":"Wos, L., Carson, D., and Robinson, G.A. The unit preference strategy in theorem proving. In Fall Joint Computer Conference, AFIPS, Washington D.C., pages 615\u2013621. Spartan Books, 1964. Reprinted in [18].","DOI":"10.1145\/1464052.1464109"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45744-5_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T21:50:49Z","timestamp":1556920249000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45744-5_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540422549","9783540457442"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-45744-5_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2001]]}}}