{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,22]],"date-time":"2025-04-22T00:29:31Z","timestamp":1745281771054},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540613770"},{"type":"electronic","value":"9783540685074"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61377-3_53","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T16:35:56Z","timestamp":1330274156000},"page":"452-467","source":"Crossref","is-referenced-by-count":3,"title":["Theorem proving modulo associativity"],"prefix":"10.1007","author":[{"given":"Albert","family":"Rubio","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"26_CR1","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4684-7118-2","volume-title":"Canonical equational proofs","author":"L. Bachmair","year":"1991","unstructured":"Leo Bachmair. Canonical equational proofs. Birkh\u00e4user, Boston, Mass., 1991."},{"key":"26_CR2","doi-asserted-by":"crossref","first-page":"192","DOI":"10.1007\/3-540-17220-3_17","volume-title":"Rewriting Techniques and Applications","author":"L. Bachmair","year":"1987","unstructured":"Leo Bachmair and Nachum Dershowitz. Completion for rewriting modulo a congruence. In Pierre Lescanne, editor, Rewriting Techniques and Applications, [2nd International Conference], LNCS 256, pages 192\u2013203, Bordeaux, France, May 25\u201327, 1987. Springer-Verlag."},{"issue":"3","key":"26_CR3","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1093\/logcom\/4.3.217","volume":"4","author":"L. Bachmair","year":"1994","unstructured":"Leo Bachmair and Harald Ganzinger. Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation, 4(3):1\u201331, 1994.","journal-title":"Journal of Logic and Computation"},{"key":"26_CR4","first-page":"244","volume-title":"Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics","author":"N. Dershowitz","year":"1990","unstructured":"Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, chapter 6, pages 244\u2013320. Elsevier Science Publishers B.V., Amsterdam, New York, Oxford, Tokyo, 1990."},{"issue":"4","key":"26_CR5","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 ACM, 27(4):797\u2013821, October 1980.","journal-title":"Journal of the ACM"},{"key":"26_CR6","doi-asserted-by":"crossref","unstructured":"Jean-Pierre Jouannaud. Confluent and coherent equational term rewriting systems: Applications to proofs in abstract data types. In Proc. 8th Colloquium on Trees in Algebra and Programming, LNCS 59, pages 269\u2013283. Springer-Verlag, 1983.","DOI":"10.1007\/3-540-12727-5_16"},{"key":"26_CR7","doi-asserted-by":"crossref","first-page":"1155","DOI":"10.1137\/0215084","volume":"15","author":"J. Jouannaud","year":"1986","unstructured":"Jean-Pierre Jouannaud and H\u00e9l\u00e8ne Kirchner. Completion of a set of rules modulo a set of equations. SIAM Journal of Computing, 15:1155\u20131194, 1986.","journal-title":"SIAM Journal of Computing"},{"key":"26_CR8","volume-title":"Technical Report Memo ATP-39","author":"D. S. Lankford","year":"1977","unstructured":"D. S. Lankford and A. M. Ballantyne. Decision procedures for simple equational theories with commutative-associative axioms: Complete sets of commutative-associative reductions. Technical Report Memo ATP-39, Dept. of Mathematics and Computer Science, Univ. of Texas, Austin, TX, August 1977."},{"issue":"2","key":"26_CR9","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1070\/SM1977v032n02ABEH002376","volume":"32","author":"G.S. Makanin","year":"1977","unstructured":"G.S. Makanin. The problem of solvability of equations in a free semigroup. Math. USSR Sbornik, 32(2):129\u2013198, 1977.","journal-title":"Math. USSR Sbornik"},{"key":"26_CR10","doi-asserted-by":"crossref","unstructured":"Paliath Narendran and Michael Rusinowitch. Any ground associative commutative theory has a finite canonical system. In Fourth int. conf. on Rewriting Techniques and Applications, LNCS 488, pages 423\u2013434, Como, Italy, April 1991. Springer-Verlag.","DOI":"10.1007\/3-540-53904-2_115"},{"key":"26_CR11","doi-asserted-by":"crossref","unstructured":"Robert Nieuwenhuis and Albert Rubio. Basic superposition is complete. In B. Krieg-Br\u00fcckner, editor, European Symposium on Programming, LNCS 582, pages 371\u2013390, Rennes, France, February 26\u201328, 1992. Springer-Verlag.","DOI":"10.1007\/3-540-55253-7_22"},{"key":"26_CR12","volume-title":"AC-Superposition with constraints: No AC-unifiers needed","author":"R. Nieuwenhuis","year":"1994","unstructured":"Robert Nieuwenhuis and Albert Rubio. AC-Superposition with constraints: No AC-unifiers needed. In Allan Bundy, editor, 12th International Conference on Automated Deduction, LNAI, Nancy, France, June 1994. Springer-Verlag."},{"issue":"4","key":"26_CR13","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1006\/jsco.1995.1020","volume":"19","author":"R. Nieuwenhuis","year":"1995","unstructured":"Robert Nieuwenhuis and Albert Rubio. Theorem Proving with Ordering and Equality Constrained Clauses. J. of Symbolic Computation, 19(4):321\u2013351, April 1995.","journal-title":"J. of Symbolic Computation"},{"issue":"2","key":"26_CR14","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1145\/322248.322251","volume":"28","author":"G.E. Peterson","year":"1981","unstructured":"G.E. Peterson and M.E. Stickel. Complete sets of reductions for some equational theories. Journal Assoc. Comput. Mach., 28(2):233\u2013264, 1981.","journal-title":"Journal Assoc. Comput. Mach."},{"key":"26_CR15","volume-title":"PhD. Thesis","author":"A. Rubio","year":"1994","unstructured":"Albert Rubio. Automated deduction with ordering and equality constrained clauses. PhD. Thesis, Technical University of Catalonia, Barcelona, Spain, 1994."},{"issue":"2","key":"26_CR16","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1016\/0304-3975(94)00276-2","volume":"142","author":"A. Rubio","year":"1995","unstructured":"Albert Rubio and Robert Nieuwenhuis. A total AC-compatible ordering based on RPO. Theoretical Computer Science, 142(2):209\u2013227, May 15, 1995.","journal-title":"Theoretical Computer Science"},{"key":"26_CR17","volume-title":"Associative Commutative Deduction with constraints","author":"L. Vigneron","year":"1994","unstructured":"Laurent Vigneron. Associative Commutative Deduction with constraints. In Allan Bundy, editor, 12th International Conference on Automated Deduction, LNAI, Nancy, France, June 1994. Springer-Verlag."}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61377-3_53.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T21:31:45Z","timestamp":1619559105000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61377-3_53"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540613770","9783540685074"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-61377-3_53","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}