{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T02:06:40Z","timestamp":1725674800206},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540502937"},{"type":"electronic","value":"9783642740640"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1988]]},"DOI":"10.1007\/978-3-642-74064-0_18","type":"book-chapter","created":{"date-parts":[[2012,4,12]],"date-time":"2012-04-12T10:52:09Z","timestamp":1334227929000},"page":"169-178","source":"Crossref","is-referenced-by-count":1,"title":["On The Unnecessity of Multiple Overlaps in Completion Theorem Proving"],"prefix":"10.1007","author":[{"given":"J\u00fcrgen","family":"M\u00fcller","sequence":"first","affiliation":[]},{"given":"Rolf","family":"Socher-Ambrosius","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"volume-title":"Inference Rules for Rewrite\u2013Based First Order Theorem Proving","year":"1987","author":"L Bachmair","key":"18_CR1","unstructured":"Bachmair, L. & Dershowitz, N. (1987). Inference Rules for Rewrite\u2013Based First Order Theorem Proving. Proc. 2nd Annual Symp. on Logic in Comp. Sci. Ithaca, N.Y"},{"volume-title":"Symbolic Logic and Mechanical Theorem Proving","year":"1973","author":"CL Chang","key":"18_CR2","unstructured":"Chang, C.L.& Lee, R.C.T. (1973). Symbolic Logic and Mechanical Theorem Proving. Academic Press, New York"},{"key":"18_CR3","first-page":"62","volume-title":"Relating Resolution and Algebraic Completion for Horn Logic","author":"R Dietrich","year":"1986","unstructured":"Dietrich, R. (1986). Relating Resolution and Algebraic Completion for Horn Logic. In: J. Siekmann (Ed.): Proc. 8th International Conference on Automated Deduction, Oxford, England. Springer LNCS 230, 62\u201378"},{"volume-title":"Some Basic Notions of First\u2013Order Unification Theory","year":"1983","author":"A Herold","key":"18_CR4","unstructured":"Herold, A. (1983). Some Basic Notions of First\u2013Order Unification Theory. MEMO-SEKI-VIII, Universit\u00e4t Karlsruhe"},{"volume-title":"Topics in Automated Theorem Proving and Program Generation","year":"1982","author":"J Hsiang","key":"18_CR5","unstructured":"Hsiang, J. (1982). Topics in Automated Theorem Proving and Program Generation. Ph. D. Thesis, Dep. of Comp. Sci., University of Illinois at Urbana-Champaign"},{"key":"18_CR6","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1016\/0004-3702(85)90074-8","volume":"25","author":"J Hsiang","year":"1985","unstructured":"Hsiang, J. (1985). Refutational Theorem Proving using Term-rewriting Systems. Artificial Intelligence 25, 255 \u2013 300","journal-title":"Artificial Intelligence"},{"volume-title":"Computational Problems in Universal Algebra","year":"1970","author":"DE Knuth","key":"18_CR7","unstructured":"Knuth, D.E. & Bendix, P.B. (1970). Simple Word Problems in Universal Algebra, in: J. Leech (Ed.): Computational Problems in Universal Algebra, Pergamon Press"},{"volume-title":"An Equational Approach to Theorem Proving in First-Order Predicate Calculus. 84CRD322","year":"1985","author":"D Kapur","key":"18_CR8","unstructured":"Kapur, D. & Narendran, P. (1985). An Equational Approach to Theorem Proving in First-Order Predicate Calculus. 84CRD322, General Electric Corp. Research and Development Report, Schenectady, N.Y"},{"key":"18_CR9","first-page":"489","volume-title":"NP-Completeness of the Set Unification and Matching Problems","author":"D Kapur","year":"1986","unstructured":"Kapur, D. & Narendran, P. (1986). NP-Completeness of the Set Unification and Matching Problems. In: J. Siekmann (Ed.): Proc. 8th International Conference on Automated Deduction, Oxford, England. Springer LNCS 230, 489 \u2013 495"},{"volume-title":"THEOPOGLES \u2013 A Theorem Prover Based on First Order Polynomials and a Special Knuth\u2013Bendix Procedure","year":"1987","author":"J M\u00fcller","key":"18_CR10","unstructured":"M\u00fcller, J. (1987). THEOPOGLES \u2013 A Theorem Prover Based on First Order Polynomials and a Special Knuth\u2013Bendix Procedure. In: K. Morik (Ed.): Proc. of 11th German Workshop on Artificial Intelligence, Geseke. Springer IFB 152"},{"volume-title":"Topics in Completion Theorem Proving","year":"1988","author":"J M\u00fcller","key":"18_CR11","unstructured":"M\u00fcller, J. & Socher, R. (1988). Topics in Completion Theorem Proving. SEKI-Report, Universit\u00e4t Kaiserslautern. (To appear)"},{"key":"18_CR12","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1016\/0022-0000(78)90043-0","volume":"16","author":"M Paterson","year":"1978","unstructured":"Paterson, M. & Wegman, M. (1978). Linear Unification. Journal of Computer and Systems Science. 16, 158 \u2013 167","journal-title":"Journal of Computer and Systems Science."}],"container-title":["Informatik-Fachberichte","K\u00fcnstliche Intelligenz"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-74064-0_18.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,25]],"date-time":"2020-11-25T02:31:03Z","timestamp":1606271463000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-74064-0_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1988]]},"ISBN":["9783540502937","9783642740640"],"references-count":12,"URL":"http:\/\/dx.doi.org\/10.1007\/978-3-642-74064-0_18","relation":{},"ISSN":["0343-3005"],"issn-type":[{"type":"print","value":"0343-3005"}],"subject":[],"published":{"date-parts":[[1988]]}}}