{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:03:22Z","timestamp":1725663802957},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540545071"},{"type":"electronic","value":"9783540384205"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1991]]},"DOI":"10.1007\/3-540-54507-7_15","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T17:56:27Z","timestamp":1330192587000},"page":"185-199","source":"Crossref","is-referenced-by-count":1,"title":["Automated deduction with associative commutative operators"],"prefix":"10.1007","author":[{"given":"M.","family":"Rusinowitch","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"L.","family":"Vigneron","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"key":"15_CR1","doi-asserted-by":"crossref","first-page":"533","DOI":"10.1007\/3-540-51081-8_131","volume":"355","author":"S. Anantharaman","year":"1989","unstructured":"Siva Anantharaman, Jieh Hsiang, and Jalel Mzali. Sbreve2: A term rewriting laboratory with (AC-)unfailing completion. In N. Dershowitz, editor, Proceedings 3rd Conference on Rewriting Techniques and Applications, Chapel Hill, (North Carolina, USA), volume 355 of Lecture Notes in Computer Science, pages 533\u2013537. Springer-Verlag, April 1989.","journal-title":"Lecture Notes in Computer Science"},{"issue":"1","key":"15_CR2","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1007\/BF00297251","volume":"4","author":"H.-J. B\u00fcrckert","year":"1988","unstructured":"H.-J. B\u00fcrckert, A. Herold, D. Kapur, J. Siekmann, M. Stickel, M. Tepp, and H. Zhang. Opening the AC-unification race. Journal of Automated Reasoning, 4(1):465\u2013474, 1988.","journal-title":"Journal of Automated Reasoning"},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"L. Bachmair and D. Plaisted. Associative path orderings. In Proceedings 1st Conference on Rewriting Techniques and Applications, Dijon (France), volume 202 of Lecture Notes in Computer Science. Springer-Verlag, 1985.","DOI":"10.1007\/3-540-15976-2_11"},{"key":"15_CR4","doi-asserted-by":"crossref","first-page":"412","DOI":"10.1137\/0204036","volume":"4","author":"D. Brand","year":"1975","unstructured":"D. Brand. Proving theorems with the modification method. SIAM J. of Computing, 4:412\u2013430, 1975.","journal-title":"SIAM J. of Computing"},{"issue":"2","key":"15_CR5","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1016\/0167-6423(87)90030-X","volume":"9","author":"A. B. Cherifa","year":"1987","unstructured":"A. Ben Cherifa 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":"15_CR6","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","volume":"17","author":"N. Dershowitz","year":"1982","unstructured":"N. Dershowitz. Orderings for term-rewriting systems. Theoretical Computer Science, 17:279\u2013301, 1982.","journal-title":"Theoretical Computer Science"},{"key":"15_CR7","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. In J. Siekmann, editor, Proceedings 8th International Conference on Automated Deduction, Oxford (UK), volume 230 of Lecture Notes in Computer Science, pages 141\u2013152. Springer-Verlag, 1986.","journal-title":"Lecture Notes in Computer Science"},{"key":"15_CR8","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1007\/3-540-18088-5_6","volume":"267","author":"J. Hsiang","year":"1987","unstructured":"J. Hsiang and M. Rusinowitch. On word problem in equational theories. In Th. Ottmann, editor, Proceedings of 14th International Colloquium on Automata, Languages and Programming, Karlsruhe (Germany), volume 267 of Lecture Notes in Computer Science, pages 54\u201371. Springer-Verlag, 1987.","journal-title":"Lecture Notes in Computer Science"},{"issue":"4","key":"15_CR9","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. Preliminary version in Proceedings 11th ACM Symposium on Principles of Programming Languages, Salt Lake City, 1984.","journal-title":"SIAM Journal of Computing"},{"key":"15_CR10","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":"15_CR11","doi-asserted-by":"crossref","first-page":"144","DOI":"10.1007\/3-540-19242-5_12","volume":"308","author":"E. Kounalis","year":"1987","unstructured":"E. Kounalis and M. Rusinowitch. On word problem in Horn logic. In J.-P. Jouannaud and S. Kaplan, editors, Proceedings 1st International Workshop on Conditional Term Rewriting Systems, Orsay (France), volume 308 of Lecture Notes in Computer Science, pages 144\u2013160. Springer-Verlag, 1987. See also the extended version published in Journal of Symbolic Computation, number 1 & 2, 1991.","journal-title":"Lecture Notes in Computer Science"},{"key":"15_CR12","unstructured":"D.S. Lankford. A unification algorithm for abelian group theory. Technical report, Louisiana Tech. University, 1979."},{"key":"15_CR13","unstructured":"D.S. Lankford and A. Ballantyne. Decision procedures for simple equational theories with associative commutative axioms: complete sets of associative commutative reductions. Technical report, Univ. of Texas at Austin, Dept. of Mathematics and Computer Science, 1977."},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"P. Narendran and M. Rusinowitch. Any ground associative-commutative theory has a finite canonical system. In R. Book, editor, Proceedings 4th Conference on Rewriting Techniques and Applications, Como, (Italy). Springer-Verlag, 1991.","DOI":"10.1007\/3-540-53904-2_115"},{"issue":"1","key":"15_CR15","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1137\/0212006","volume":"12","author":"G. Peterson","year":"1983","unstructured":"G. Peterson. A technique for establishing completeness results in theorem proving with equality. SIAM Journal of Computing, 12(1):82\u2013100, 1983.","journal-title":"SIAM Journal of Computing"},{"key":"15_CR16","first-page":"73","volume":"7","author":"G. Plotkin","year":"1972","unstructured":"G. Plotkin. Building-in equational theories. Machine Intelligence, 7:73\u201390, 1972.","journal-title":"Machine Intelligence"},{"key":"15_CR17","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":"15_CR18","unstructured":"M. Rusinowitch. D\u00e9monstration automatique-Techniques de r\u00e9\u00e9criture. InterEditions, 1989."},{"key":"15_CR19","first-page":"135","volume":"4","author":"G. Robinson","year":"1969","unstructured":"G. Robinson and L.T. Wos. Paramodulation and first-order theorem proving. In B. Meltzer and D. Mitchie, editors, Machine Intelligence 4, pages 135\u2013150. Edinburgh University Press, 1969.","journal-title":"Machine Intelligence"},{"key":"15_CR20","doi-asserted-by":"crossref","first-page":"372","DOI":"10.1007\/3-540-53162-9_52","volume":"463","author":"J. Steinbach","year":"1990","unstructured":"J. Steinbach. Ac-termination of rewrite systems \u2014 A modified Knuth-Bendix ordering. In H. Kirchner and W. Wechler, editors, Proceedings 2nd International Conference on Algebraic and Logic Programming, Nancy (France), volume 463 of Lecture Notes in Computer Science, pages 372\u2013386. Springer-Verlag, 1990.","journal-title":"Lecture Notes in Computer Science"},{"key":"15_CR21","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1145\/322261.322262","volume":"28","author":"M. Stickel","year":"1981","unstructured":"M. Stickel. A unification algorithm for associative-commutative functions. Journal of the Association for Computing Machinery, 28:423\u2013434, 1981.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"15_CR22","doi-asserted-by":"crossref","unstructured":"M. Stickel. A case study of theorem proving by the knuth-bendix method Discovering that x 3=x implies ring commutativity. In Proceedings 7th International Conference on Automated Deduction, volume 170 of Lecture Notes in Computer Science. Springer-Verlag, 1984.","DOI":"10.1007\/978-0-387-34768-4_15"},{"key":"15_CR23","unstructured":"L. Vigneron. Deduction automatique dans des th\u00e9ories associatives-commutatives. Rapport interne, Centre de Recherche en Informatique de Nancy, Vand\u0153uvre-l\u00e8s-Nancy, 1990."}],"container-title":["Lecture Notes in Computer Science","Fundamentals of Artificial Intelligence Research"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-54507-7_15.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T15:55:19Z","timestamp":1605628519000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-54507-7_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991]]},"ISBN":["9783540545071","9783540384205"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/3-540-54507-7_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1991]]}}}