{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:13:05Z","timestamp":1725664385418},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540603818"},{"type":"electronic","value":"9783540455134"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60381-6_1","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T18:22:40Z","timestamp":1330280560000},"page":"1-14","source":"Crossref","is-referenced-by-count":8,"title":["Associative-commutative superposition"],"prefix":"10.1007","author":[{"given":"Leo","family":"Bachmair","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Harald","family":"Ganzinger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,25]]},"reference":[{"key":"1_CR1","doi-asserted-by":"crossref","unstructured":"L. Bachmair, N. Dershowitz and D. Plaisted, 1989. Completion without failure. In H. Ait-Kaci, M. Nivat, editors, Resolution of Equations in Algebraic Structures, vol. 2, pp. 1\u201330. Academic Press.","DOI":"10.1016\/B978-0-12-046371-8.50007-9"},{"key":"1_CR2","first-page":"427","volume-title":"Lecture Notes in Computer Science, vol. 449","author":"L. Bachmair","year":"1990","unstructured":"L. Bachmair and H. Ganzinger, 1990. On Restrictions of Ordered Paramodulation with Simplification. In M. Stickel, editor, Proc. 10th Int. Conf. on Automated Deduction, Kaiserslautern, Lecture Notes in Computer Science, vol. 449, pp. 427\u2013441, Berlin, Springer-Verlag."},{"key":"1_CR3","first-page":"384","volume-title":"Technical Report MPI-I-93-249","author":"L. Bachmair","year":"1993","unstructured":"L. Bachmair and H. Ganzinger, 1993. Rewrite Techniques for Transitive Relations. Technical Report MPI-I-93-249, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken. Short version in Proc. LICS'94, pp. 384\u2013393, 1994."},{"issue":"No.3","key":"1_CR4","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1093\/logcom\/4.3.217","volume":"4","author":"L. Bachmair","year":"1994","unstructured":"L. Bachmair and H. Ganzinger, 1994. Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation, Vol. 4, No. 3, pp. 217\u2013247. Revised version of Technical Report MPI-I-91-208, 1991.","journal-title":"Journal of Logic and Computation"},{"key":"1_CR5","series-title":"Automated Deduction \u2014 CADE'11","first-page":"462","volume-title":"Lecture Notes in Computer Science, vol. 607","author":"L. Bachmair","year":"1992","unstructured":"L. Bachmair, H. Ganzinger, Chr. Lynch and W. Snyder, 1992. Basic Paramodulation and Superposition. In D. Kapur, editor, Automated Deduction \u2014 CADE'11, Lecture Notes in Computer Science, vol. 607, pp. 462\u2013476, Berlin, Springer-Verlag."},{"issue":"No.3\/4","key":"1_CR6","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1007\/BF01190829","volume":"5","author":"L. Bachmair","year":"1994","unstructured":"Leo Bachmair, Harald Ganzinger and Uwe Waldmann, 1994. Refutational Theorem Proving for Hierarchic First-Order Theories. Applicable Algebra in Engineering, Communication and Computing, Vol. 5, No. 3\/4, pp. 193\u2013212. Earlier version: Theorem Proving for Hierarchic First-Order Theories, in Giorgio Levi and H\u00e9l\u00e8ne Kirchner, editors, Algebraic and Logic Programming, Third International Conference, LNCS 632, pages 420\u2013434, Volterra, Italy, September 2\u20134, 1992, Springer-Verlag.","journal-title":"Applicable Algebra in Engineering, Communication and Computing"},{"key":"1_CR7","first-page":"29","volume-title":"Lecture Notes in Computer Science, vol. 355","author":"T. Baird","year":"1989","unstructured":"Timothy Baird, Gerald Peterson and Ralph Wilkerson, 1989. Complete sets of reductions modulo associativity, commutativity and identity. In Proc. 3rd Int. Conf. on Rewriting Techniques and Applications, Lecture Notes in Computer Science, vol. 355, pp. 29\u201344, Berlin, Springer-Verlag."},{"key":"1_CR8","first-page":"243","volume-title":"Handbook of Theoretical Computer Science B: Formal Methods and Semantics","author":"N. Dershowitz","year":"1990","unstructured":"N. Dershowitz and J.-P. Jouannaud, 1990. Rewrite Systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science B: Formal Methods and Semantics, chapter 6, pp. 243\u2013309. North-Holland, Amsterdam."},{"issue":"No.3","key":"1_CR9","doi-asserted-by":"publisher","first-page":"559","DOI":"10.1145\/116825.116833","volume":"38","author":"J. Hsiang","year":"1991","unstructured":"J. Hsiang and M. Rusinowitch, 1991. Proving refutational completeness of theorem proving strategies: The transfinite semantic Tree method. Journal of the ACM, Vol. 38, No. 3, pp. 559\u2013587.","journal-title":"Journal of the ACM"},{"key":"1_CR10","first-page":"54","volume-title":"Lecture Notes in Computer Science, vol. 267","author":"J. Hsiang","year":"1987","unstructured":"Jieh Hsiang and Michael Rusinowitch, 1987. On Word Problems in Equational Theories. In Proc. 14th ICALP, Lecture Notes in Computer Science, vol. 267, pp. 54\u201371, Berlin, Springer-Verlag."},{"key":"1_CR11","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/0304-3975(92)90165-C","volume":"104","author":"J. Jouannaud","year":"1992","unstructured":"Jean-Pierre Jouannaud and Claude March\u00e9, 1992. Termination and completion modulo associativity, commutativity and identity. Theoretical Computer Science, Vol. 104, pp. 29\u201351.","journal-title":"Theoretical Computer Science"},{"key":"1_CR12","volume-title":"Any Ground Associative-Commutative Theory has a Finite Canonical System","author":"P. Narendran","year":"1991","unstructured":"Paliath Narendran and Micha\u00ebl Rusinowitch, 1991. Any Ground Associative-Commutative Theory has a Finite Canonical System. In Ronald V. Book, editor, Proc. 4th Rewriting Techniques and Applications 91, Como, Italy, Springer-Verlag."},{"key":"1_CR13","first-page":"371","volume-title":"Lecture Notes in Computer Science, vol. 582","author":"R. Nieuwenhuis","year":"1992","unstructured":"R. Nieuwenhuis and A. Rubio, 1992. Basic superposition is complete. In ESOP'92, Lecture Notes in Computer Science, vol. 582, pp. 371\u2013389, Berlin, Springer-Verlag."},{"key":"1_CR14","first-page":"545","volume-title":"Lecture Notes in Computer Science, vol. 814","author":"R. Nieuwenhuis","year":"1994","unstructured":"R. Nieuwenhuis and A. Rubio, 1994. AC-superposition with constraints: No AC-unifiers needed. In Proc. 12th International Conference on Automated Deduction, Lecture Notes in Computer Science, vol. 814, pp. 545\u2013559, Berlin, Springer-Verlag."},{"key":"1_CR15","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/S0747-7171(08)80130-7","volume":"11","author":"J. Pais","year":"1991","unstructured":"John Pais and G.E. Peterson, 1991. Using Forcing to Prove Completeness of resolution and Paramodulation. Journal of Symbolic Computation, Vol. 11, pp. 3\u201319.","journal-title":"Journal of Symbolic Computation"},{"key":"1_CR16","doi-asserted-by":"crossref","first-page":"577","DOI":"10.1016\/S0747-7171(19)80003-2","volume":"14","author":"E. Paul","year":"1992","unstructured":"E. Paul, 1992. A general refutational completeness result for an inference procedure based on associative-commutative unification. Journal of Symbolic Computation, Vol. 14, pp. 577\u2013618.","journal-title":"Journal of Symbolic Computation"},{"key":"1_CR17","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1145\/322248.322251","volume":"28","author":"G. Peterson","year":"1981","unstructured":"G. Peterson and M. Stickel, 1981. Complete sets of reductions for some equational theories. Journal of the ACM, Vol. 28, pp. 233\u2013264.","journal-title":"Journal of the ACM"},{"key":"1_CR18","first-page":"374","volume-title":"Lecture Notes in Computer Science, vol. 690","author":"A. Rubio","year":"1993","unstructured":"A. Rubio and R. Nieuwenhuis, 1993. A precedence-based total AC-compatible ordering. In Proc. 5th Int. Conf. on Rewriting Techniques and Applications, Lecture Notes in Computer Science, vol. 690, pp. 374\u2013388, Berlin, Springer-Verlag."},{"key":"1_CR19","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1016\/S0747-7171(08)80131-9","volume":"11","author":"M. Rusinowitch","year":"1991","unstructured":"M. Rusinowitch, 1991. Theorem proving with resolution and superposition: An extension of the Knuth and Bendix completion procedure as a complete set of inference rules. J. Symbolic Computation, Vol. 11, pp. 21\u201349.","journal-title":"J. Symbolic Computation"},{"key":"1_CR20","first-page":"185","volume-title":"Lecture Notes in Artificial Intelligence, vol. 535","author":"M. Rusinowitch","year":"1991","unstructured":"M. Rusinowitch and L. Vigneron, 1991. Automated deduction with associative-commutative operators. In Proc. Int. Workshop on Fundamentals of Artificial Intelligence Research, Lecture Notes in Artificial Intelligence, vol. 535, pp. 185\u2013199, Berlin, Springer-Verlag."},{"key":"1_CR21","first-page":"530","volume-title":"Lecture Notes in Computer Science, vol. 814","author":"L. Vigneron","year":"1994","unstructured":"L. Vigneron, 1994. Associative-commutative dedution with constraints. In Proc. 12th International Conference on Automated Deduction, Lecture Notes in Computer Science, vol. 814, pp. 530\u2013544, Berlin, Springer-Verlag."},{"key":"1_CR22","volume-title":"Technical Report MPI-I-92-216","author":"U. Wertz","year":"1992","unstructured":"U. Wertz, 1992. First-Order Theorem Proving Modulo Equations. Technical Report MPI-I-92-216, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken."},{"key":"1_CR23","volume-title":"PhD thesis","author":"H. Zhang","year":"1988","unstructured":"H. Zhang, 1988. Reduction, superposition and induction: Automated reasoning in an equational logic. PhD thesis, Rensselaer Polytechnic Institute, Schenectady, New York."}],"container-title":["Lecture Notes in Computer Science","Conditional and Typed Rewriting Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60381-6_1.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,31]],"date-time":"2021-12-31T09:45:53Z","timestamp":1640943953000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60381-6_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540603818","9783540455134"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/3-540-60381-6_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}