{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:00:57Z","timestamp":1767927657073,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540368342","type":"print"},{"value":"9783540368359","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11805618_22","type":"book-chapter","created":{"date-parts":[[2006,7,25]],"date-time":"2006-07-25T14:29:13Z","timestamp":1153837753000},"page":"287-296","source":"Crossref","is-referenced-by-count":15,"title":["Slothrop: Knuth-Bendix Completion with a Modern Termination Checker"],"prefix":"10.1007","author":[{"given":"Ian","family":"Wehrman","sequence":"first","affiliation":[]},{"given":"Aaron","family":"Stump","sequence":"additional","affiliation":[]},{"given":"Edwin","family":"Westbrook","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"22_CR1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F. Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)"},{"key":"22_CR2","doi-asserted-by":"crossref","unstructured":"Bachmair, L.: Canonical Equational Proofs. In: Progress in Theoretical Computer Science. Birkh\u00e4user (1991)","DOI":"10.1007\/978-1-4684-7118-2"},{"key":"22_CR3","first-page":"1","volume-title":"Resolution of Equations in Algebraic Structures, Rewriting Techniques","author":"L. Bachmair","year":"1989","unstructured":"Bachmair, L., Dershowitz, N., Plaisted, D.A.: Completion Without Failure. In: Resolution of Equations in Algebraic Structures, Rewriting Techniques, vol.\u00a02, pp. 1\u201330. Academic Press, London (1989)"},{"key":"22_CR4","unstructured":"Contejean, E., March\u00e9, C., Urbain, X.: CiME3 (2004), available at: \n                    \n                      http:\/\/cime.lri.fr\/"},{"key":"22_CR5","unstructured":"Filli\u00e2tre, J.-C.: Ocaml data structures, available at: \n                    \n                      http:\/\/www.lri.fr\/~filliatr\/software.en.html"},{"key":"22_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1007\/978-3-540-25979-4_15","volume-title":"Rewriting Techniques and Applications","author":"J. Giesl","year":"2004","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Automated Termination Proofs with AProVE. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol.\u00a03091, pp. 210\u2013220. Springer, Heidelberg (2004)"},{"issue":"1","key":"22_CR7","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1016\/0022-0000(81)90002-7","volume":"23","author":"G. Huet","year":"1981","unstructured":"Huet, G.: A Complete Proof of Correctness of the Knuth-Bendix Completion Algorithm. Journal of Computer and System Science\u00a023(1), 11\u201321 (1981)","journal-title":"Journal of Computer and System Science"},{"key":"22_CR8","first-page":"263","volume-title":"Computational Problems in Abstract Algebra","author":"D. Knuth","year":"1970","unstructured":"Knuth, D., Bendix, P.: Simple Word Problems in Universal Algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, pp. 263\u2013297. Pergamon Press, Oxford (1970)"},{"key":"22_CR9","series-title":"Lecture Notes in Artificial Intelligence","first-page":"486","volume-title":"Automated Deduction - CADE-18","author":"B. L\u00f6chner","year":"2002","unstructured":"L\u00f6chner, B., Hillenbrand, T.: The Next Waldmeister Loop. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 486\u2013500. Springer, Heidelberg (2002)"},{"key":"22_CR10","series-title":"Lecture Notes in Computer Science","first-page":"176","volume-title":"STACS 94","author":"A. Sattler-Klein","year":"1994","unstructured":"Sattler-Klein, A.: About Changing the Ordering During Knuth-Bendix Completion. In: Enjalbert, P., Mayr, E.W., Wagner, K.W. (eds.) STACS 1994. LNCS, vol.\u00a0775, pp. 176\u2013186. Springer, Heidelberg (1994)"},{"key":"22_CR11","doi-asserted-by":"crossref","unstructured":"Stump, A., L\u00f6chner, B.: Knuth-Bendix Completion of Theories of Commuting Group Endomorphisms. In: Information Processing Letters (to appear, 2006)","DOI":"10.1016\/j.ipl.2006.01.009"},{"key":"22_CR12","unstructured":"Wehrman, I., Stump, A.: Mining Propositional Simplification Proofs for Small Validating Clauses. In: Armando, A., Cimatti, A. (eds.) 3rd International Workshop on Pragmatics of Decision Procedures in Automated Reasoning (2005)"}],"container-title":["Lecture Notes in Computer Science","Term Rewriting and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11805618_22.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:26:01Z","timestamp":1619508361000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11805618_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540368342","9783540368359"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/11805618_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}