{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:25:54Z","timestamp":1761611154873},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[1995,1,1]],"date-time":"1995-01-01T00:00:00Z","timestamp":788918400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["AAECC"],"published-print":{"date-parts":[[1995,1]]},"DOI":"10.1007\/bf01270929","type":"journal-article","created":{"date-parts":[[2005,3,24]],"date-time":"2005-03-24T22:11:05Z","timestamp":1111702265000},"page":"23-56","source":"Crossref","is-referenced-by-count":16,"title":["Automated deduction with associative-commutative operators"],"prefix":"10.1007","volume":"6","author":[{"given":"Micha\ufffdl","family":"Rusinowitch","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Laurent","family":"Vigneron","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","first-page":"533","volume-title":"Lecture Notes in Computer Science","author":"S. Anantharaman","year":"1989","unstructured":"Anantharaman, S., Hsiang, J., Mzali, J.: Sbreve2: A term rewriting laboratory with (AC-)unfailing completion. In: Dershowitz, N. (ed) Proceedings 3rd Conference on Rewriting Techniques and Applications, Chapel Hill (N.C., USA), vol. 355. Lecture Notes in Computer Science, pp. 533?537. Berlin, Heidelberg, New York: Springer 1989"},{"issue":"2?3","key":"CR2","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1016\/0304-3975(89)90003-0","volume":"67","author":"L. Bachmair","year":"1989","unstructured":"Bachmair, L., Dershowitz, N.: Completion for rewriting modulo a congruence. Theoret. Comput. Sci.67(2?3), 173?202 (1989)","journal-title":"Theoret. Comput. Sci."},{"key":"CR3","first-page":"427","volume-title":"Lecture Notes in Computer Science","author":"L. Bachmair","year":"1990","unstructured":"Bachmair, L., Ganzinger, H.: On restrictions of ordered paramodulation with simplification. In: Stickel, M. E. (ed) Proceedings 10th International Conference on Automated Deduction, Kaiserslautern (Germany), vol. 449. Lecture Notes in Computer Science, pp. 427?411. Berlin, Heidelberg, New York: Springer 1990"},{"issue":"1","key":"CR4","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1007\/BF00297251","volume":"4","author":"H.-J. B\u00fcrckert","year":"1988","unstructured":"B\u00fcrckert, H.-J., Herold, A., Kapur, D., Siekmann, J., Stickel, M. E., Tepp, M., Zhang, H.: Opening the AC-unification race. J. Automated Reasoning4(1), 465?474 (1988)","journal-title":"J. Automated Reasoning"},{"key":"CR5","volume-title":"Lecture Notes in Computer Science","author":"L. Bachmair","year":"1985","unstructured":"Bachmair, L., Plaisted, D.: Associative path orderings. In: Proceedings 1st Conference on Rewriting Techniques and Applications, Dijon (France), vol. 202. Lecture Notes in Computer Science. Berlin, Heidelberg, New York: Springer 1985"},{"key":"CR6","doi-asserted-by":"crossref","first-page":"412","DOI":"10.1137\/0204036","volume":"4","author":"D. Brand","year":"1975","unstructured":"Brand, D.: Proving theorems with the modification method. SIAM J. Comput.4, 412?430 (1975)","journal-title":"SIAM J. Comput."},{"key":"CR7","first-page":"386","volume-title":"Lecture Notes in Computer Science","author":"R. B\u00fcndgen","year":"1991","unstructured":"B\u00fcndgen, R.: Simulating Buchberger's algorithm by Knuth-Bendix completion. In: Book, R. (ed) Proceedings 4th Conference on Rewriting Techniques and Applications, Como (Italy), vol. 448. Lecture Notes in Computer Science, pp. 386?397. Berlin, Heidelberg, New York: Springer 1991"},{"issue":"2","key":"CR8","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1016\/0167-6423(87)90030-X","volume":"9","author":"A. Ben Cherifa","year":"1987","unstructured":"Cherifa, A. Ben, Lescanne, P.: Termination of rewriting systems by polynomial interpretations and its implementation. Sci. Comput. Programming9(2), 137?159 (1987)","journal-title":"Sci. Comput. Programming"},{"key":"CR9","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","volume":"17","author":"N. Dershowitz","year":"1982","unstructured":"Dershowitz, N.: Orderings for term-rewriting systems. Theoret. Comput. Sci.17, 279?301 (1982)","journal-title":"Theoret. Comput. Sci."},{"key":"CR10","unstructured":"Domenjoud, E.: Outils pour la d\u00e9duction automatique dans les th\u00e9ories associatives-commutatives. Th\u00e9se de Doctorat d'Universit\u00e9, Universit\u00e9 de Nancy I, September 1991"},{"key":"CR11","first-page":"54","volume-title":"Lecture Notes in Computer Science","author":"J. Hsiang","year":"1987","unstructured":"Hsiang, J., Rusinowitch, M.: On word problem in equational theories. In: Ottmann, T. (ed) Proceedings of 14th International Colloquium on Automata, Languages and Programming, Karlsruhe (Germany), vol. 267. Lecture Notes in Computer Science, pp. 54?71. Berlin, Heidelberg, New York: Springer 1987"},{"issue":"3","key":"CR12","doi-asserted-by":"crossref","first-page":"559","DOI":"10.1145\/116825.116833","volume":"38","author":"J. Hsiang","year":"1991","unstructured":"Hsiang, J., Rusinowitch, M.: Proving Refutational Completenss of Theorem-Proving Strategies: The Transfinite Semantic Tree Method. Journal of the Association for Computing Machinery38(3), 559?587 (1991)","journal-title":"Journal of the Association for Computing Machinery"},{"issue":"4","key":"CR13","doi-asserted-by":"crossref","first-page":"1155","DOI":"10.1137\/0215084","volume":"15","author":"J.-P. Jouannaud","year":"1986","unstructured":"Jouannaud, J.-P., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM Journal of Computing15(4), 1155?1194 (1986). Preliminary version in Proceedings 11th ACM Symposium on Principles of Programming Languages, Salt Lake City (USA), 1984","journal-title":"SIAM Journal of Computing"},{"key":"CR14","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1016\/B978-0-08-012975-4.50028-X","volume-title":"Computational Problems in Abstract Algebra","author":"D. E. Knuth","year":"1970","unstructured":"Knuth, D. E., Bendix, P. B.: Simple word problems in universal algebras. In: Leech, J. (ed) Computational Problems in Abstract Algebra, pp. 263?297. Oxford: Pergamon Press 1970"},{"key":"CR15","first-page":"214","volume-title":"Proceedings 6th IEEE symposium on Logic in Computer Science (LICS)","author":"D. Kozen","year":"1991","unstructured":"Kozen, D.: A completeness theorem for kleene algebras and the algebra of regular events. In: Proceedings 6th IEEE symposium on Logic in Computer Science (LICS), pp. 214?225. IEEE Computer Society Press, Los Alamitos, July 1991"},{"key":"CR16","first-page":"114","volume-title":"Lecture Notes in Computer Science","author":"E. Kounalis","year":"1987","unstructured":"Kounalis, E., Rusinowitch, M.: On word problem in Horn logic. In: Jouannaud, J.-P., Kaplan, S. (eds) Proceedings 1st International Workshop on Conditional Term Rewriting Systems, Orsay (France), vol. 308. Lecture Notes in Computer Science, pp. 114?160. Berlin, Heidelbeg, New York: Springer 1987. See also the extended version published in J. Symb. Comput.11(1,2), (1991)"},{"key":"CR17","first-page":"187","volume-title":"Lecture Notes in Computer Science","author":"M. Lai","year":"1989","unstructured":"Lai, M.: On how to move mountains ?associatively and commutatively?. In: Dershowitz, N. (ed) Proceedings 3rd Conference on Rewriting Techniques and Applications, Chapel Hill (N.C., USA), vol. 355. Lecture Notes in Computer Science, pp 187?202. Berlin, Heidelberg, New York: Springer 1989"},{"key":"CR18","unstructured":"Lankford, D. S.: Mechanical theorem proving in field theory. Technical report, Louisiana Tech. University, 1979"},{"key":"CR19","volume-title":"Technical report","author":"D. S. Lankford","year":"1979","unstructured":"Lankford, D. S.: On proving term rewriting systems are noetherian. Technical report, Louisiana Tech. University, Mathematics Dept., Ruston LA, 1979"},{"key":"CR20","volume-title":"Technical report","author":"D. S. Lankford","year":"1977","unstructured":"Lankford, D. S., Ballantyne, A.: 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":"CR21","volume-title":"Automatic Theorem Proving","author":"D. Loveland","year":"1978","unstructured":"Loveland, D.: Automatic Theorem Proving. North-Holland: Elsevier Science 1978"},{"key":"CR22","first-page":"423","volume-title":"Lecture Notes in Computer Science vol. 488","author":"P. Narendran","year":"1991","unstructured":"Narendran, P., Rusinowitch, M.: Any Ground Associative-Commutative Theory has a Finite Canonical System. In: Book, R. V. (ed) Proceedings 4th International Conference Rewriting Techniques and Applications, pp. 423?434, Como (Italy). Lecture Notes in Computer Science vol. 488. Berlin, Heidelberg, New York: Springer 1991"},{"issue":"6","key":"CR23","doi-asserted-by":"crossref","first-page":"557","DOI":"10.1016\/S0747-7171(19)80003-2","volume":"14","author":"E. Paul","year":"1992","unstructured":"Paul, E.: A general refutational completeness result for an inference procedure based on associative-commutative unification. J. Symb. Comput.14(6), 557?618 (1992)","journal-title":"J. Symb. Comput."},{"issue":"1","key":"CR24","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1137\/0212006","volume":"12","author":"G. Peterson","year":"1983","unstructured":"Peterson, G.: A technique for establishing completeness results in theorem proving with equality. SIAM J. Comput.12(1), 82?100 (1983)","journal-title":"SIAM J. Comput."},{"key":"CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"156","DOI":"10.1007\/3-540-54507-7_13","volume-title":"Fundamental of Artificial Intelligence Research, vol. 535","author":"U. Petermann","year":"1991","unstructured":"Petermann, U.: Building in equational theories into the connection method. In: Jorrand, P., Kelemen, J. (eds) Fundamental of Artificial Intelligence Research, vol. 535. Lecture Notes in Computer Science, pp. 156?169. Berlin, Heidelberg, New York: Springer 1991"},{"key":"CR26","first-page":"73","volume":"7","author":"G. Plotkin","year":"1972","unstructured":"Plotkin, G.: Building-in equational theories. Machine Intelligence.7, 73?90 (1972)","journal-title":"Machine Intelligence."},{"issue":"1,2","key":"CR27","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/S0747-7171(08)80130-7","volume":"11","author":"J. Pais","year":"1991","unstructured":"Pais, J., Peterson, G. E.: Using forcing to prove completeness of resolution and paramodulation. Journal of Symbolic Computation11(1,2): 3?19 (1991)","journal-title":"Journal of Symbolic Computation"},{"key":"CR28","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1145\/322248.322251","volume":"28","author":"G. Peterson","year":"1981","unstructured":"G. Peterson, Stickel, M. E.: Complete sets of reductions for some equational theories. Journal of the Association for Computing Machinery28, 233?264 (1981)","journal-title":"Journal of the Association for Computing Machinery"},{"key":"CR29","unstructured":"Rusinowitch, M.: D\u00e9monstration automatique-Techniques de r\u00e9\u00e9criture. Inter Editions 1989"},{"key":"CR30","first-page":"185","volume-title":"Lecture Notes in Artificial Intelligence, subseries of Lecture Notes in Computer Science vol. 535","author":"M. Rusinowitch","year":"1991","unstructured":"Rusinowitch, M., Vigneron, L.: Automated Deduction with Associative Commutative Operators. In: Jorrand, P., Kelemen, J. (eds) Proceedings International Workshop Fundamentals of Artifical Intelligence Research, pp. 185?199, Smolenice (Czechoslovakia), September 1991. Berlin, Heidelberg, New York: Springer. Lecture Notes in Artificial Intelligence, subseries of Lecture Notes in Computer Science vol. 535"},{"key":"CR31","unstructured":"Robinson, G. A., Wos, L. T.: Paramodulation and first-order theorem proving. In: Meltzer, B., Mitchie, D. (eds) Machine Intelligence vol. 4, pp. 135?150. Edinburgh University Press 1969"},{"key":"CR32","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1145\/322261.322262","volume":"28","author":"M. E. Stickel","year":"1981","unstructured":"Stickel, M. E.: A unification algorithm for associative-commutative functions. J. Assoc. Comput. Machinery28, 423?434 (1981)","journal-title":"J. Assoc. Comput. Machinery"},{"key":"CR33","first-page":"248","volume-title":"Lecture Notes in Computer Science","author":"M. E. Stickel","year":"1984","unstructured":"Stickel, M. E.: A case study of theorem proving by the Knuth-Bendix method: Discovering thatx 3 =x implies ring commutativity. In: Shostak, R. (ed) Proceedings 7th International Conference on Automated Deduction, Napa Valley (Calif., USA), vol. 170. Lecture Notes in Computer Science, pp. 248?258. Berlin, Heidelberg, New York: Springer 1984"},{"key":"CR34","unstructured":"Wertz, U.: First-order theorem proving modulo equations. Technical Report MPI-I-92-216, Max Planck Institut f\u00fcr Informatik, April 1992"}],"container-title":["Applicable Algebra in Engineering, Communication and Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01270929.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01270929\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01270929","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,6]],"date-time":"2020-04-06T13:36:07Z","timestamp":1586180167000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01270929"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,1]]},"references-count":34,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1995,1]]}},"alternative-id":["BF01270929"],"URL":"https:\/\/doi.org\/10.1007\/bf01270929","relation":{},"ISSN":["0938-1279","1432-0622"],"issn-type":[{"value":"0938-1279","type":"print"},{"value":"1432-0622","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995,1]]}}}