{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,14]],"date-time":"2025-07-14T02:44:20Z","timestamp":1752461060195},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540581567"},{"type":"electronic","value":"9783540484677"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58156-1_39","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T15:22:48Z","timestamp":1330269768000},"page":"530-544","source":"Crossref","is-referenced-by-count":14,"title":["Associative-commutative deduction with constraints"],"prefix":"10.1007","author":[{"given":"Laurent","family":"Vigneron","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,30]]},"reference":[{"key":"39_CR1","first-page":"427","volume-title":"On restrictions of ordered paramodulation with simplification","author":"L. Bachmair","year":"1990","unstructured":"L. Bachmair and H. Ganzinger. On restrictions of ordered paramodulation with simplification. In M. E. Stickel, editor, Proc. 10th CADE Conf., Kaiserslautern (Germany), volume 449 of LNCS, pages 427\u2013441. Springer-Verlag, July 1990."},{"key":"39_CR2","doi-asserted-by":"crossref","unstructured":"L. Bachmair, H. Ganzinger, C. Lynch, and W. Snyder. Basic paramodulation and superposition. In Proc. 11th CADE Conf., Saratoga Springs (N.Y., USA), pages 462\u2013476, 1992.","DOI":"10.1007\/3-540-55602-8_185"},{"key":"39_CR3","unstructured":"A. M. Ballantyne and D. S. Lankford. The refutation completeness of blocked permutative narrowing and resolution. In Proc. of Fourth Workshop on Automated Deduction, Austin, Texas, 1979."},{"key":"39_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"},{"key":"39_CR5","volume-title":"Handbook of Theoretical Computer Science","author":"N. Dershowitz","year":"1990","unstructured":"N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science. Elsevier Science Publishers B. V. (North-Holland), 1990."},{"key":"39_CR6","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1145\/321495.321500","volume":"16","author":"J. R. Guard","year":"1969","unstructured":"J. R. Guard, F. C. Oglesby, J. H. Bennett, and Settle. Semi-automated mathematics. JACM, 16:49\u201362, 1969.","journal-title":"JACM"},{"issue":"3","key":"39_CR7","doi-asserted-by":"crossref","first-page":"559","DOI":"10.1145\/116825.116833","volume":"38","author":"J. Hsiang","year":"1991","unstructured":"J. Hsiang and M. Rusinowitch. Proving refutational completeness of theorem-proving strategies: the transfinite semantic tree method. JACM, 38(3):559\u2013587, July 1991.","journal-title":"JACM"},{"key":"39_CR8","volume-title":"Compilation de Formes Canoniques dans les Th\u00e9ories \u00e9quationelles","author":"J.-M. Hullot","year":"1980","unstructured":"J.-M. Hullot. Compilation de Formes Canoniques dans les Th\u00e9ories \u00e9quationelles. Th. 3e cycle, Universit\u00e9 de Paris Sud, Orsay (France), 1980."},{"key":"39_CR9","first-page":"257","volume-title":"Computational Logic. Essays in honor of Alan Robinson, chapter 8","author":"J.-P. Jouannaud","year":"1991","unstructured":"J.-P. Jouannaud and C. Kirchner. Solving equations in abstract algebras: a rule-based survey of unification. In J.-L. Lassez and G. Plotkin, editors, Computational Logic. Essays in honor of Alan Robinson, chapter 8, pages 257\u2013321. MIT Press, Cambridge (MA, USA), 1991."},{"issue":"3","key":"39_CR10","first-page":"9","volume":"4","author":"C. Kirchner","year":"1990","unstructured":"C. Kirchner, H. Kirchner, and M. Rusinowitch. Deduction with symbolic constraints. Revue d'Intelligence Artificielle, 4(3):9\u201352, 1990. Special issue on Automatic Deduction.","journal-title":"Revue d'Intelligence Artificielle"},{"key":"39_CR11","volume-title":"Only prime superpositions need be considered in the Knuth-Bendix procedure","author":"D. Kapur","year":"1985","unstructured":"D. Kapur, D. R. Musser, and P. Narendran. Only prime superpositions need be considered in the Knuth-Bendix procedure, 1985. Computer Science Branch, Corporate Research and Development, General Electric, Schenectady, New York."},{"key":"39_CR12","first-page":"704","volume-title":"Proc. 9th CADE Conf.","author":"W. McCune","year":"1988","unstructured":"W. McCune. Challenge equality problems in lattice theory. In E. Lusk and R. Overbeek, editors, Proc. 9th CADE Conf., Argonne (Ill., USA), volume 310 of LNCS, pages 704\u2013709. Springer-Verlag, 1988."},{"key":"39_CR13","volume-title":"Proc. 10th CADE Conf.","author":"U. Martin","year":"1990","unstructured":"U. Martin and T. Nipkow. Ordered rewriting and confluence. In M. E. Stickel, editor, Proc. 10th CADE Conf., Kaiserslautern (Germany), volume 449 of LNCS. Springer-Verlag, 1990."},{"key":"39_CR14","volume-title":"Proc. 4th RTA Conf.","author":"P. Narendran","year":"1991","unstructured":"P. Narendran and M. Rusinowitch. Any ground associative-commutative theory has a finite canonical system. In R. V. Book, editor, Proc. 4th RTA Conf., Como (Italy). Springer-Verlag, 1991."},{"key":"39_CR15","doi-asserted-by":"crossref","unstructured":"R. Nieuwenhuis and A. Rubio. Basic superposition is complete. In B. Krieg-Br\u00fcckner, editor, Proceedings of ESOP'92, volume 582 of LNCS, pages 371\u2013389. Springer-Verlag, 1992.","DOI":"10.1007\/3-540-55253-7_22"},{"key":"39_CR16","doi-asserted-by":"crossref","unstructured":"R. Nieuwenhuis and A. Rubio. Theorem proving with ordering constrained clauses. In D. Kapur, editor, Proceedings of CADE-11, volume 607 of LNCS, pages 477\u2013491. Springer-Verlag, 1992. [NR94] R. Nieuwenhuis and A. Rubio. AC-superposition with constraints: no AC-unifiers needed. In A. Bundy, editor, Proceedings of the 12th International Conference on Automated Deduction, Nancy (France), LNCS. Springer-Verlag, 1994.","DOI":"10.1007\/3-540-58156-1_40"},{"issue":"6","key":"39_CR17","first-page":"577","volume":"14","author":"E. Paul","year":"1992","unstructured":"E. Paul. A general refutational completeness result for an inference procedure based on associative-commutative unification. JSC, 14(6):577\u2013618, 1992.","journal-title":"JSC"},{"issue":"1","key":"39_CR18","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 J. of Computing, 12(1):82\u2013100, 1983.","journal-title":"SIAM J. of Computing"},{"key":"39_CR19","first-page":"381","volume-title":"Proc. 10th CADE Conf.","author":"G. E. Peterson","year":"1990","unstructured":"G. E. Peterson. Complete sets of reductions with constraints. In M. E. Stickel, editor, Proc. 10th CADE Conf., Kaiserslautern (Germany), volume 449 of LNCS, pages 381\u2013395. Springer-Verlag, 1990."},{"key":"39_CR20","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":"39_CR21","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1145\/322248.322251","volume":"28","author":"G. Peterson","year":"1981","unstructured":"G. Peterson and M. E. Stickel. Complete sets of reductions for some equational theories. JACM, 28:233\u2013264, 1981.","journal-title":"JACM"},{"key":"39_CR22","first-page":"374","volume-title":"Proc. 5th RTA Conf.","author":"A. Rubio","year":"1993","unstructured":"A. Rubio and R. Nieuwenhuis. A precedence-based total ac-compatible ordering. In C. Kirchner, editor, Proc. 5th RTA Conf., Montreal (Canada), volume 690 of LNCS, pages 374\u2013388. Springer-Verlag, 1993."},{"key":"39_CR23","first-page":"21","volume":"11","author":"M. Rusinowitch","year":"1991","unstructured":"M. Rusinowitch. Theorem-proving with resolution and superposition. JSC, 11:21\u201349, 1991.","journal-title":"JSC"},{"key":"39_CR24","doi-asserted-by":"crossref","unstructured":"M. Rusinowitch and L. Vigneron. Automated deduction with associative commutative operators. In P. Jorrand and J. Kelemen, editors, Fundamental of Artificial Intelligence Research, volume 535 of LNCS, pages 185\u2013199. Springer-Verlag, 1991.","DOI":"10.1007\/3-540-54507-7_15"},{"key":"39_CR25","unstructured":"M. Rusinowitch and L. Vigneron. Automated deduction with associative commutative operators. Internal rep. 1896, INRIA, May 1993. To appear in J. of Applicable Algebra in Engineering, Communication and Computation."},{"issue":"4","key":"39_CR26","doi-asserted-by":"crossref","first-page":"622","DOI":"10.1145\/321850.321859","volume":"21","author":"J. R. Slagle","year":"1974","unstructured":"J. R. Slagle. Automated theorem-proving for theories with simplifiers, commutativity and associativity. JACM, 21(4):622\u2013642, 1974.","journal-title":"JACM"},{"key":"39_CR27","unstructured":"L. Vigneron. Basic AC-paramodulation. In F. Orejas, editor, Proc. 2nd CCL Workshop, La Escala (Spain), September 1993."},{"key":"39_CR28","unstructured":"U. Wertz. First-order theorem proving modulo equations. Technical Report MPI-I-92-216, MPI Informatik, April 1992."},{"key":"39_CR29","first-page":"1","volume-title":"Proc. 9th CADE Conf.","author":"H. Zhang","year":"1988","unstructured":"H. Zhang and D. Kapur. First-order theorem proving using conditional rewrite rules. In E. Lusk and R. Overbeek, editors, Proc. 9th CADE Conf., Argonne (Ill., USA), volume 310 of LNCS, pages 1\u201320. Springer-Verlag, 1988."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-12"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58156-1_39.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:17:39Z","timestamp":1605647859000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58156-1_39"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540581567","9783540484677"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/3-540-58156-1_39","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}