{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:02:34Z","timestamp":1767927754003,"version":"3.49.0"},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"3","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2013,3]]},"DOI":"10.1007\/s10817-012-9249-2","type":"journal-article","created":{"date-parts":[[2012,4,13]],"date-time":"2012-04-13T04:01:44Z","timestamp":1334289704000},"page":"317-354","source":"Crossref","is-referenced-by-count":8,"title":["Multi-Completion with Termination Tools"],"prefix":"10.1007","volume":"50","author":[{"given":"Sarah","family":"Winkler","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Haruhiko","family":"Sato","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aart","family":"Middeldorp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Masahito","family":"Kurihara","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,4,14]]},"reference":[{"key":"9249_CR1","doi-asserted-by":"crossref","unstructured":"Alarc\u00f3n, B., Guti\u00e9rrez, R., Iborra, J., Lucas, S.: Proving termination of context-sensitive rewriting with MU-TERM. In: Proc. 6th PROLE. ENTCS, vol.\u00a0188, pp.\u00a0105\u2013115 (2007)","DOI":"10.1016\/j.entcs.2007.05.041"},{"key":"9249_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"},{"issue":"1","key":"9249_CR3","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S0747-7171(88)80018-X","volume":"6","author":"L Bachmair","year":"1988","unstructured":"Bachmair, L., Dershowitz, N.: Critical pair criteria for completion. J. Symb. Comput. 6(1), 1\u201318 (1988)","journal-title":"J. Symb. Comput."},{"issue":"2","key":"9249_CR4","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1145\/174652.174655","volume":"41","author":"L Bachmair","year":"1994","unstructured":"Bachmair, L., Dershowitz, N.: Equational inference, canonical proofs, and proof orderings. J. ACM 41(2), 236\u2013276 (1994)","journal-title":"J. ACM"},{"key":"9249_CR5","doi-asserted-by":"crossref","unstructured":"B\u00fcndgen, R., G\u00f6bel, M., K\u00fcchlin, W.: A fine-grained parallel completion procedure. In: Proc. 7th ISSAC, pp.\u00a0269\u2013277 (1994)","DOI":"10.1145\/190347.190427"},{"key":"9249_CR6","doi-asserted-by":"crossref","unstructured":"Christian, J.: Fast Knuth\u2013Bendix completion. In Proc. 3rd RTA. LNCS, vol.\u00a0355, pp.\u00a0551\u2013555 (1989)","DOI":"10.1007\/3-540-51081-8_136"},{"key":"9249_CR7","doi-asserted-by":"crossref","first-page":"629","DOI":"10.1137\/0217039","volume":"17","author":"N Dershowitz","year":"1988","unstructured":"Dershowitz, N., Marcus, L., Tarlecki, A.: Existence, uniqueness, and construction of rewrite systems. SIAM J. Comput. 17, 629\u2013639 (1988)","journal-title":"SIAM J. Comput."},{"key":"9249_CR8","doi-asserted-by":"crossref","unstructured":"Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: Automatic termination proofs in the dependency pair framework. In: Proc. 3rd IJCAR. LNAI, vol. 4130, pp.\u00a0281\u2013286 (2006)","DOI":"10.1007\/11814771_24"},{"key":"9249_CR9","doi-asserted-by":"crossref","unstructured":"Graf, P.: Term indexing. In: LNAI, vol.\u00a01053. Springer (1996)","DOI":"10.1007\/3-540-61040-5"},{"issue":"1","key":"9249_CR10","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1016\/S0747-7171(88)80019-1","volume":"6","author":"D Kapur","year":"1988","unstructured":"Kapur, D., Musser, D.R., Narendran, P.: Only prime superpositions need be considered in the Knuth\u2013Bendix completion procedure. J. Symb. Comput. 6(1), 19\u201336 (1988)","journal-title":"J. Symb. Comput."},{"key":"9249_CR11","unstructured":"Klein, D., Hirokawa, N.: Maximal completion (system description). In: Proc. 22nd RTA. LIPIcs, vol.\u00a010 pp.\u00a071\u201380 (2011)"},{"key":"9249_CR12","doi-asserted-by":"crossref","unstructured":"Knuth, D.E., Bendix, P.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, pp.\u00a0263\u2013297. Pergamon Press (1970)","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"9249_CR13","doi-asserted-by":"crossref","unstructured":"Korp, M., Sternagel, C., Zankl, H., Middeldorp, A.: Tyrolean termination tool 2. In: Proc. 20th RTA. LNCS, vol.\u00a05595, pp.\u00a0295\u2013304 (2009)","DOI":"10.1007\/978-3-642-02348-4_21"},{"key":"9249_CR14","doi-asserted-by":"crossref","unstructured":"K\u00fcchlin, W.: A confluence criterion based on the generalised Newman lemma. In: Proc. 2nd EUROCAL. LNCS, vol.\u00a0204, pp.\u00a0390\u2013399 (1985)","DOI":"10.1007\/3-540-15984-3_294"},{"issue":"1","key":"9249_CR15","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1023\/A:1006129631807","volume":"23","author":"M Kurihara","year":"1999","unstructured":"Kurihara, M., Kondo, H.: Completion for multiple reduction orderings. J. Autom. Reason. 23(1), 25\u201342 (1999)","journal-title":"J. Autom. Reason."},{"key":"9249_CR16","doi-asserted-by":"crossref","unstructured":"Lescanne, P.: REVE: a rewrite rule laboratory. In: Proc. 4th International Symposium on Theoretical Aspects of Computer Science. LNCS, vol.\u00a0247, pp.\u00a0482\u2013483 (1987)","DOI":"10.1007\/BFb0039637"},{"key":"9249_CR17","doi-asserted-by":"crossref","unstructured":"March\u00e9, C.: Normalized rewriting: An unified view of Knuth\u2013Bendix completion and Gr\u00f6bner bases computation. In: Symbolic Rewriting Techniques. Progress in Computer Science and Applied Logic, vol.\u00a015, pp.\u00a0193\u2013208. Birkh\u00e4user (1998)","DOI":"10.1007\/978-3-0348-8800-4_9"},{"issue":"2","key":"9249_CR18","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/BF00245458","volume":"9","author":"W McCune","year":"1992","unstructured":"McCune, W.: Experiments with discrimination-tree indexing and path indexing for term retrieval. J. Autom. Reason. 9(2), 147\u2013167 (1992)","journal-title":"J. Autom. Reason."},{"issue":"1","key":"9249_CR19","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1016\/0020-0190(83)90009-1","volume":"16","author":"Y M\u00e9tivier","year":"1983","unstructured":"M\u00e9tivier, Y.: About the rewriting systems produced by the Knuth\u2013Bendix completion algorithm. Inform. Process. Lett. 16(1), 31\u201334 (1983)","journal-title":"Inform. Process. Lett."},{"key":"9249_CR20","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Handbook of Automated Reasoning, pp.\u00a0371\u2013443. Elsevier Science (2001)","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"key":"9249_CR21","doi-asserted-by":"crossref","unstructured":"Sato, H., Winkler, S., Kurihara, M., Middeldorp, A.: Multi-completion with termination tools (system description). In: Proc. 4th IJCAR. LNAI, vol.\u00a05195, pp.\u00a0306\u2013312 (2008)","DOI":"10.1007\/978-3-540-71070-7_26"},{"issue":"2","key":"9249_CR22","first-page":"220","volume":"E92-D","author":"H Sato","year":"2009","unstructured":"Sato, H., Winkler, S., Kurihara, M., Middeldorp, A.: Constraint-based multi-completion procedures for term rewriting systems. IEICE Trans. Electron. E92-D(2), 220\u2013234 (2009)","journal-title":"IEICE Trans. Electron."},{"key":"9249_CR23","doi-asserted-by":"crossref","unstructured":"Sattler-Klein, A.: About changing the ordering during Knuth\u2013Bendix completion. In: Proc. 11th STACS. LNCS, vol.\u00a0775, pp.\u00a0175\u2013186 (1994)","DOI":"10.1007\/3-540-57785-8_140"},{"key":"9249_CR24","doi-asserted-by":"crossref","unstructured":"Sekar, R., Ramakrishnan, I.V., Voronkov, A.: Term indexing. In: Handbook of Automated Reasoning, pp.\u00a01853\u20131964. Elsevier Science (2001)","DOI":"10.1016\/B978-044450813-3\/50028-X"},{"key":"9249_CR25","unstructured":"Steinbach, J., K\u00fchler, U.: Check Your Ordering\u2014Termination Proofs and Open Problems. Technical Report SR-90-25, Universit\u00e4t Kaiserslautern (1990)"},{"issue":"5","key":"9249_CR26","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1016\/j.ipl.2006.01.009","volume":"98","author":"A Stump","year":"2006","unstructured":"Stump, A., L\u00f6chner, B.: Knuth\u2013Bendix completion of theories of commuting group endomorphisms. Inform. Process. Lett. 98(5), 195\u2013198 (2006)","journal-title":"Inform. Process. Lett."},{"issue":"4","key":"9249_CR27","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","volume":"43","author":"G Sutcliffe","year":"2009","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure: the FOF and CNF parts, v3.5.0. J. Autom. Reason. 43(4), 337\u2013362 (2009)","journal-title":"J. Autom. Reason."},{"issue":"2","key":"9249_CR28","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1007\/BF00881918","volume":"15","author":"A Voronkov","year":"1995","unstructured":"Voronkov, A.: The anatomy of Vampire. J. Autom. Reason. 15(2), 237\u2013265 (1995)","journal-title":"J. Autom. Reason."},{"key":"9249_CR29","doi-asserted-by":"crossref","unstructured":"Voronkov, A.: Algorithms, datastructures, and other issues in efficient automated deduction. In: Proc. 1st IJCAR. LNCS, vol.\u00a02083, pp.\u00a013\u201328 (2001)","DOI":"10.1007\/3-540-45744-5_3"},{"key":"9249_CR30","doi-asserted-by":"crossref","unstructured":"Wehrman, I.: Knuth\u2013Bendix completion with modern termination checking. Master\u2019s thesis, Washington University in St.\u00a0Louis, 2006. Technical report WUCSE-2006-45","DOI":"10.1007\/11805618_22"},{"key":"9249_CR31","doi-asserted-by":"crossref","unstructured":"Wehrman, I., Stump, A.: Mining propositional simplification proofs for small validating clauses. In: Proc. 3rd PDPAR. ENTCS, vol.\u00a0144, pp.\u00a079\u201391 (2005)","DOI":"10.1016\/j.entcs.2005.12.008"},{"key":"9249_CR32","doi-asserted-by":"crossref","unstructured":"Wehrman, I., Stump, A., Westbrook, E.M.: Slothrop: Knuth\u2013Bendix completion with a modern termination checker. In: Proc. 17th RTA. LNCS, vol.\u00a04098, pp.\u00a0287\u2013296 (2006)","DOI":"10.1007\/11805618_22"},{"key":"9249_CR33","doi-asserted-by":"crossref","unstructured":"Winkler, F.: Reducing the complexity of the Knuth\u2013Bendix completion-algorithm: a \u201cunification\u201d of different approaches. In: Proc. 2nd EUROCAL. LNCS, vol.\u00a0204, pp.\u00a0378\u2013389 (1985)","DOI":"10.1007\/3-540-15984-3_293"},{"key":"9249_CR34","doi-asserted-by":"crossref","unstructured":"Winkler, S., Middeldorp, A.: Termination tools in ordered completion. In: Proc. 5th IJCAR. LNAI, vol.\u00a06173, pp.\u00a0518\u2013532 (2010)","DOI":"10.1007\/978-3-642-14203-1_43"},{"key":"9249_CR35","doi-asserted-by":"crossref","unstructured":"Winkler, S., Middeldorp, A.: AC completion with termination tools. In: Proc. 23rd CADE. LNAI, vol.\u00a06803, pp.\u00a0492\u2013498 (2011)","DOI":"10.1007\/978-3-642-22438-6_37"},{"key":"9249_CR36","unstructured":"Winkler, S., Sato, H., Middeldorp, A., Kurihara, M.: Optimizing mkbTT (system description). In: Proc. 21st RTA. LIPIcs, vol.\u00a06, pp.\u00a0373\u2013384 (2010)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-012-9249-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,27]],"date-time":"2019-06-27T06:41:15Z","timestamp":1561617675000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-012-9249-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,4,14]]},"references-count":36,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2013,3]]}},"alternative-id":["9249"],"URL":"https:\/\/doi.org\/10.1007\/s10817-012-9249-2","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,4,14]]}}}