{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:48:03Z","timestamp":1749124083452},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540539049"},{"type":"electronic","value":"9783540463832"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1991]]},"DOI":"10.1007\/3-540-53904-2_115","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T17:16:24Z","timestamp":1330190184000},"page":"423-434","source":"Crossref","is-referenced-by-count":26,"title":["Any ground associative-commutative theory has a finite canonical system"],"prefix":"10.1007","author":[{"given":"Paliath","family":"Narendran","sequence":"first","affiliation":[]},{"given":"Micha\u00ebl","family":"Rusinowitch","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"35_CR1","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1007\/BF00302643","volume":"6","author":"S. Anantharaman","year":"1990","unstructured":"S. Anantharaman and J. Hsiang. An automated proof of the moufong identities in alternative rings. J. Automated Reasoning, 6:79\u2013109, 1990.","journal-title":"J. Automated Reasoning"},{"key":"35_CR2","doi-asserted-by":"crossref","unstructured":"L. Bachmair and N. Dershowitz. Commutation, transformation and termination. In J. Siekmann, editor, Proceedings 8th Conf. on Automated Deduction, pages 5\u201320, Springer-Verlag, 1986. Lecture Notes in Computer Science, volume 230.","DOI":"10.1007\/3-540-16780-3_76"},{"key":"35_CR3","unstructured":"L. Bachmair, N. Dershowitz, and J. Hsiang. Orderings for equational proofs. In Proceedings Symp. Logic in Computer Science, pages 346\u2013357, Boston (Massachusetts USA), 1986."},{"key":"35_CR4","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1016\/0898-1221(81)90115-2","volume":"7","author":"A.M. Ballantyne","year":"1981","unstructured":"A.M. Ballantyne and D. Lankford. New decision algorithms for finitely presented commutative semigroups. Comp. & Maths. with Appl., 7:159\u2013165, 1981.","journal-title":"Comp. & Maths. with Appl."},{"issue":"2","key":"35_CR5","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1016\/0167-6423(87)90030-X","volume":"9","author":"A. BenCherifa","year":"1987","unstructured":"A. BenCherifa and P. Lescanne. Termination of rewriting systems by polynomial interpretations and its implementation. Science of Computer Programming, 9(2):137\u2013160, October 1987.","journal-title":"Science of Computer Programming"},{"key":"35_CR6","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1016\/S0747-7171(85)80019-5","volume":"1","author":"L. Bachmair","year":"1985","unstructured":"L. Bachmair and D.A. Plaisted. Termination orderings for associative-commutative rewriting systems. Journal of Symbolic Computation, 1:329\u2013349, 1985.","journal-title":"Journal of Symbolic Computation"},{"key":"35_CR7","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/S0747-7171(87)80022-6","volume":"1","author":"N. Dershowitz","year":"1987","unstructured":"N. Dershowitz. Termination of Rewriting. Journal of Symbolic Computation, 1 & 2:69\u2013116, 1987.","journal-title":"Journal of Symbolic Computation"},{"key":"35_CR8","doi-asserted-by":"crossref","unstructured":"N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In Van Leuven, editor, Handbook of Theoretical Computer Science, North Holland, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"35_CR9","doi-asserted-by":"crossref","first-page":"413","DOI":"10.2307\/2370405","volume":"XXXV","author":"L. Dickson","year":"1913","unstructured":"L. Dickson. Finiteness of the odd perfect and primitive abundant numbers with n distinct prime factors. Amer. J. Math., XXXV:413\u2013422, 1913.","journal-title":"Amer. J. Math."},{"key":"35_CR10","doi-asserted-by":"crossref","unstructured":"J. Gallier, P. Narendran, D. Plaisted, S. Raatz, and W. Snyder. Finding canonical rewriting systems equivalent to a finite set of ground equations in polynomial time. In E. Lusk and R. Overbeek, editors, Proceedings 9th Int. Conf. on Automated Deduction, pages 182\u2013196, Springer-Verlag, Lecture Notes in Computer Science, 1988.","DOI":"10.1007\/BFb0012832"},{"key":"35_CR11","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1007\/3-540-16780-3_86","volume":"230","author":"J. Hsiang","year":"1986","unstructured":"J. Hsiang, and M. Rusinowitch. A new method for establishing refutational completeness in theorem proving. Proceedings of the 8th Conference on Automated Deduction, LNCS 230 (1986) 141\u2013152.","journal-title":"Proceedings of the 8th Conference on Automated Deduction, LNCS"},{"issue":"4","key":"35_CR12","doi-asserted-by":"crossref","first-page":"797","DOI":"10.1145\/322217.322230","volume":"27","author":"G. Huet","year":"1980","unstructured":"G. Huet. Confluent reductions: abstract properties and applications to term rewriting systems. Journal of the Association for Computing Machinery, 27(4):797\u2013821, October 1980.","journal-title":"Journal of the Association for Computing Machinery"},{"issue":"4","key":"35_CR13","doi-asserted-by":"crossref","first-page":"1155","DOI":"10.1137\/0215084","volume":"15","author":"J.-P. Jouannaud","year":"1986","unstructured":"J.-P. Jouannaud and H. Kirchner. Completion of a set of rules modulo a set of equations. SIAM Journal of Computing, 15(4):1155\u20131194, 1986.","journal-title":"SIAM Journal of Computing"},{"key":"35_CR14","unstructured":"D. Kapur and P. Narendran. NP-completeness of the associative-commutative unification and related problems. Unpublished Manuscript, Computer Science Branch, General Electric Corporate Research and Development, Schenectady, NY, Dec. 1986."},{"key":"35_CR15","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1016\/0304-3975(85)90023-4","volume":"35","author":"D. Kapur","year":"1985","unstructured":"D. Kapur and P. Narendran. A finite Thue system with decidable word problem and without equivalent finite canonical system. Theoretical Computer Science, 35:337\u2013344, 1985.","journal-title":"Theoretical Computer Science"},{"key":"35_CR16","doi-asserted-by":"crossref","unstructured":"D. Kapur, G. Sivakumar, and H. Zhang. A New Method for Proving Termination of AC-Rewrite Systems. To be presented at the Conference on the Foundations of Software Technology and Theoretical Computer Science, New Delhi, India, December 1990.","DOI":"10.1007\/3-540-53487-3_40"},{"key":"35_CR17","first-page":"263","volume-title":"Computational Problems in Abstract Algebra","author":"D.E. Knuth","year":"1970","unstructured":"D.E. Knuth and P.B. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263\u2013297, Pergamon Press, Oxford, 1970."},{"key":"35_CR18","series-title":"Technical Report","volume-title":"On Proving Term Rewriting Systems are Noetherian","author":"D.S. Lankford","year":"1979","unstructured":"D.S. Lankford. On Proving Term Rewriting Systems are Noetherian. Technical Report, Louisiana Tech. University, Mathematics Dept., Ruston LA, 1979."},{"key":"35_CR19","unstructured":"D.S. Lankford and A. Ballantyne. Decision procedures for simple equational theories with permutative axioms: complete sets of permutative reductions. Technical Report, Univ. of Texas at Austin, Dept. of Mathematics and Computer Science, 1977."},{"key":"35_CR20","doi-asserted-by":"crossref","unstructured":"E. W. Mayr. An algorithm for the general petri net reachability problem. In Proceedings of STOC, 1981.","DOI":"10.1145\/800076.802477"},{"key":"35_CR21","unstructured":"P. Narendran and M. Rusinowitch. Unifiability in ground AC theories. 1990. In preparation."},{"key":"35_CR22","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1145\/322248.322251","volume":"28","author":"G. Peterson","year":"1981","unstructured":"G. Peterson and M. Stickel. Complete sets of reductions for some equational theories. Journal of the Association for Computing Machinery, 28:233\u2013264, 1981.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"35_CR23","doi-asserted-by":"crossref","unstructured":"W. Snyder. Efficient completion: an O(nlogn) algorithm for generating reduced sets of ground rewrite rules equivalent to a set of ground equations E. In N. Dershowitz, editor, Proceedings 3rd Conf. on Rewriting Techniques and Applications, pages \u2014, Springer-Verlag, Lecture Notes in Computer Science, 1989.","DOI":"10.1007\/3-540-51081-8_123"},{"key":"35_CR24","doi-asserted-by":"crossref","first-page":"372","DOI":"10.1007\/3-540-53162-9_52","volume":"463","author":"J. Steinbach","year":"1990","unstructured":"Steinbach, J. AC-termination of rewrite systems \u2014 A modified Knuth-Bendix ordering. Proceedings 2nd International Conference on Algebraic and Logic Programming, Nancy (France), Lecture Notes in Computer Science 463, 372\u2013386, (1990).","journal-title":"Lecture Notes in Computer Science"}],"container-title":["Lecture Notes in Computer Science","Rewriting Techniques and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-53904-2_115.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T15:51:12Z","timestamp":1605628272000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-53904-2_115"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991]]},"ISBN":["9783540539049","9783540463832"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-53904-2_115","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1991]]}}}