{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T12:58:01Z","timestamp":1648558681597},"publisher-location":"Berlin, Heidelberg","reference-count":52,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540593409","type":"print"},{"value":"9783540492375","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-59340-3_5","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:14:29Z","timestamp":1330276469000},"page":"54-73","source":"Crossref","is-referenced-by-count":3,"title":["Some extensions of rewriting"],"prefix":"10.1007","author":[{"given":"H\u00e9l\u00e8ne","family":"Kirchner","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"key":"5_CR1","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1007\/BF00302643","volume":"6","author":"S. Anantharaman","year":"1990","unstructured":"S. Anantharaman and J. Hsiang. An automated proof of the Moufang identities in alternative rings. Journal of Automated Reasoning, 6:79\u2013109, 1990.","journal-title":"Journal of Automated Reasoning"},{"key":"5_CR2","unstructured":"S. Anantharaman and J. Mzali. Unfailing completion modulo a set of equations. Research Report 470, LRI-Orsay (Fr.), 1989."},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"F. Baader and K. Schulz. Combination techniques and decision problems for disuni-fication. volume 690 of Lecture Notes in Computer Science, pages 301\u2013315. Springer-Verlag, June 1993.","DOI":"10.1007\/3-540-56868-9_23"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"L. Bachmair. Canonical equational proofs. Computer Science Logic, Progress in Theoretical Computer Science. Birkh\u00e4user Verlag AG, 1991.","DOI":"10.1007\/978-1-4684-7118-2"},{"issue":"2\u20133","key":"5_CR5","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1016\/0304-3975(89)90003-0","volume":"67","author":"L. Bachmair","year":"1989","unstructured":"L. Bachmair and N. Dershowitz. Completion for rewriting modulo a congruence. Theoretical Computer Science, 67(2\u20133):173\u2013202, October 1989.","journal-title":"Theoretical Computer Science"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"L. Bachmair, N. Dershowitz, and D. Plaisted. Completion without failure. In H. A\u00eft-Kaci and M. Nivat, editors, Resolution of Equations in Algebraic Structures, Volume 2: Rewriting Techniques, pages 1\u201330. Academic Press, 1989.","DOI":"10.1016\/B978-0-12-046371-8.50007-9"},{"key":"5_CR7","volume-title":"Technical Report MPI-I-93-250","author":"L. Bachmair","year":"1993","unstructured":"L. Bachmair and H. Ganzinger. Associative-Commutative superposition. Technical Report MPI-I-93-250, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken, 1993."},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"L. Bachmair and H. Ganzinger. Buchberger's algorithm: A constraint-based completion procedure. In Proceedings 1st International Conference on Constraints in Computational Logics, Munich (Germany), sept. 1994.","DOI":"10.1007\/BFb0016860"},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"L. Bachmair, H. Ganzinger, C. Lynch, and W. Snyder. Basic paramodulation and superposition. In Proceedings 11th International Conference on Automated Deduction, Saratoga Springs (N.Y., USA), pages 462\u2013476, 1992.","DOI":"10.1007\/3-540-55602-8_185"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"T. B. Baird, G. E. Peterson, and R. W. Wilkerson. Complete sets of reductions modulo associativity, commutativity and identity. In N. Dershowitz, editor, Proceedings 3rd Conference on Rewriting Techniques and Applications, Chapel Hill (N.C., USA), volume 355 of Lecture Notes in Computer Science, pages 29\u201344. Springer-Verlag, April 1989.","DOI":"10.1007\/3-540-51081-8_98"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"H. P. Barendregt et al. Term graph rewriting. In Proc. of PARLE'87, volume 259 of Lecture Notes in Computer Science. Springer-Verlag, 1987.","DOI":"10.1007\/3-540-17945-3_8"},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"H. Comon. Completion of rewrite systems with membership constraints. In W. Kuich, editor, Proceedings of ICALP 92, volume 623 of Lecture Notes in Computer Science. Springer-Verlag, 1992.","DOI":"10.1007\/3-540-55719-9_91"},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"N. Dershowitz and J.-P. Jouannaud. Handbook of Theoretical Computer Science, volume B, chapter 6: Rewrite Systems, pages 244\u2013320. Elsevier Science Publishers B. V. (North-Holland), 1990. Also as: Research report 478, LRI.","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"N. Dershowitz and J.-P. Jouannaud. Rewrite Systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, chapter 6, pages 244\u2013320. Elsevier Science Publishers B. V. (North-Holland), 1990.","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"5_CR15","first-page":"162","volume":"43","author":"N. Dershowitz","year":"1991","unstructured":"N. Dershowitz and J.-P. Jouannaud. Notations for rewriting. Bulletin of European Association for Theoretical Computer Science, 43:162\u2013172, February 1991.","journal-title":"Bulletin of European Association for Theoretical Computer Science"},{"key":"5_CR16","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1016\/0304-3975(90)90064-O","volume":"75","author":"N. Dershowitz","year":"1990","unstructured":"N. Dershowitz and M. Okada. A rationale for conditional equational programming. Theoretical Computer Science, 75:111\u2013138, 1990.","journal-title":"Theoretical Computer Science"},{"key":"5_CR17","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/BF00263448","volume":"8","author":"E. Domenjoud","year":"1992","unstructured":"E. Domenjoud. A technical note on AC-unification. The number of minimal unifiers of the equation \u03b1x 1+\u22ef+\u03b1x p= Ac \u03b2y 1+\u22ef+\u03b2y q. Journal of Automated Reasoning, 8:39\u201344, 1992. Also as research report CRIN 89-R-2.","journal-title":"Journal of Automated Reasoning"},{"key":"5_CR18","first-page":"53","volume-title":"Proceedings of Graph Reduction Workshop, volume 279 of Lecture Notes in Computer Science","author":"J. A. Goguen","year":"1987","unstructured":"J. A. Goguen, C. Kirchner, and J. Meseguer. Concurrent term rewriting as a model of computation. In R. Keller and J. Fasel, editors, Proceedings of Graph Reduction Workshop, volume 279 of Lecture Notes in Computer Science, pages 53\u201393, Santa Fe (NM, USA), 1987. Springer-Verlag."},{"key":"5_CR19","unstructured":"G. Huet. Constrained Resolution: A Complete Method for Higher Order Logic. PhD thesis, Case Western Reserve University, 1972."},{"issue":"4","key":"5_CR20","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. Preliminary version in 18th Symposium on Foundations of Computer Science, IEEE, 1977.","journal-title":"Journal of the ACM"},{"key":"5_CR21","first-page":"11","volume":"23","author":"G. Huet","year":"1981","unstructured":"G. Huet. A complete proof of the Knuth-Bendix completion algorithm. In JCSS 23, pages 11\u201321, 1981.","journal-title":"JCSS"},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"J. Jaffar and J.-L. Lassez. Constraint logic programming. In Proceedings of the 14th Annual ACM Symposium on Principles Of Programming Languages, Munich (Germany), pages 111\u2013119, 1987.","DOI":"10.1145\/41625.41635"},{"issue":"4","key":"5_CR23","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 (USA), 1984.","journal-title":"SIAM Journal of Computing"},{"key":"5_CR24","doi-asserted-by":"crossref","unstructured":"J.-P. Jouannaud and C. March\u00e9. Completion modulo associativity, commutativity and identity (AC1). In A. Miola, editor, Proceedings of DISCO'90, volume 429 of Lecture Notes in Computer Science, pages 111\u2013120. Springer-Verlag, April 1990.","DOI":"10.1007\/3-540-52531-9_130"},{"key":"5_CR25","doi-asserted-by":"crossref","unstructured":"S. Kaplan and J.-L. R\u00e9my. Completion algorithms for conditional rewriting systems. In H. A\u00eft-Kaci and M. Nivat, editors, Resolution of Equations in Algebraic Structures, Volume 2: Rewriting Techniques, pages 141\u2013170. Academic Press, 1989.","DOI":"10.1016\/B978-0-12-046371-8.50011-0"},{"key":"5_CR26","doi-asserted-by":"crossref","unstructured":"D. Kapur and H. Zhang. RRL: A rewrite rule laboratory. In Proceedings 9th International Conference on Automated Deduction, Argonne (Ill., USA), volume 310 of Lecture Notes in Computer Science, pages 768\u2013769. Springer-Verlag, 1988.","DOI":"10.1007\/BFb0012889"},{"key":"5_CR27","first-page":"360","volume-title":"Computational Logic. Essays in honor of Alan Robinson","author":"D. Kapur","year":"1991","unstructured":"D. Kapur and H. Zhang. A case study of the completion procedure: ring commutativity problems. In J.-L. Lassez and G. Plotkin, editors, Computational Logic. Essays in honor of Alan Robinson, chapter 10, pages 360\u2013394. MIT Press, Cambridge (MA, USA), 1991."},{"key":"5_CR28","doi-asserted-by":"crossref","unstructured":"C. Kirchner and H. Kirchner. Constrained equational reasoning. In Proceedings of the ACM-SIGSAM 1989 International Symposium on Symbolic and Algebraic Computation, Portland (Oregon), pages 382\u2013389. ACM Press, July 1989. Report CRIN 89-R-220.","DOI":"10.1145\/74540.74585"},{"key":"5_CR29","doi-asserted-by":"crossref","unstructured":"C. Kirchner, H. Kirchner, and J. Meseguer. Operational semantics of OBJ-3. In Proceedings of 15th International Colloquium on Automata, Languages and Programming, volume 317 of Lecture Notes in Computer Science, pages 287\u2013301. Springer-Verlag, 1988.","DOI":"10.1007\/3-540-19488-6_123"},{"issue":"3","key":"5_CR30","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":"5_CR31","first-page":"166","volume-title":"Implementing computational systems with constraints","author":"C. Kirchner","year":"1993","unstructured":"C. Kirchner, H. Kirchner, and M. Vittek. Implementing computational systems with constraints. In Paris Kanellakis, Jean-Louis Lassez, and Vijay Saraswat, editors, Proceedings of the first Workshop on Principles and Practice of Constraint Programming, Providence (R.I., USA), pages 166\u2013175. Brown University, 1993."},{"key":"5_CR32","first-page":"617","volume-title":"Constraint solving by narrowing in combined algebraic domains","author":"H. Kirchner","year":"1994","unstructured":"H. Kirchner and C. Ringeissen. Constraint solving by narrowing in combined algebraic domains. In P. Van Hentenryck, editor, Proceedings of the 11th International Conference on Logic Programming, S. Margherita Ligure (Italy), pages 617\u2013631, MIT Press, 1994."},{"key":"5_CR33","unstructured":"D. S. Lankford and A. Ballantyne. Decision procedures for simple equational theories with permutative axioms: complete sets of permutative reductions. Technical report, Univ. of Texas at Austin, Dept. of Mathematics and Computer Science, 1977."},{"key":"5_CR34","doi-asserted-by":"crossref","unstructured":"C. Lynch and W. Snyder. Redundancy criteria for constrained completion. In C. Kirchner, editor, Proceedings 5th Conference on Rewriting Techniques and Applications, Montreal (Canada), volume 690 of Lecture Notes in Computer Science, pages 2\u201316. Springer-Verlag, 1993.","DOI":"10.1007\/3-540-56868-9_2"},{"key":"5_CR35","volume-title":"Th\u00e8se de Doctorat d'Universit\u00e9","author":"C. March\u00e9","year":"1993","unstructured":"C. March\u00e9. R\u00e9\u00e9criture modulo une th\u00e9orie pr\u00e9sent\u00e9e par un syst\u00e8me convergent et d\u00e9cidabilit\u00e9 du probl\u00e8me du mot dans certaines classes de th\u00e9ories \u00e9quationnelles. Th\u00e8se de Doctorat d'Universit\u00e9, Universit\u00e9 de Paris-Sud, Orsay (France), October 1993."},{"key":"5_CR36","doi-asserted-by":"crossref","unstructured":"U. Martin and T. Nipkow. Ordered rewriting and confluence. In M. E. Stickel, editor, Proceedings 10th International Conference on Automated Deduction, Kaiserslautern (Germany), volume 449 of Lecture Notes in Computer Science. Springer-Verlag, 1990.","DOI":"10.1007\/3-540-52885-7_100"},{"issue":"1","key":"5_CR37","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","volume":"96","author":"J. Meseguer","year":"1992","unstructured":"J. Meseguer. Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science, 96(1):73\u2013155, 1992.","journal-title":"Theoretical Computer Science"},{"key":"5_CR38","doi-asserted-by":"crossref","unstructured":"C. K. Mohan. Priority rewriting: Semantics, confluence, and conditionals. In N. Dershowitz, editor, Proceedings 3rd Conference on Rewriting Techniques and Applications, Chapel Hill (N.C., USA), volume 355 of Lecture Notes in Computer Science, pages 278\u2013291. Springer-Verlag, April 1989.","DOI":"10.1007\/3-540-51081-8_114"},{"key":"5_CR39","doi-asserted-by":"crossref","unstructured":"P. Narendran and M. Rusinowitch. Any ground associative-commutative theory has a finite canonical system. In R. V. Book, editor, Proceedings 4th Conference on Rewriting Techniques and Applications, Como (Italy). Springer-Verlag, 1991.","DOI":"10.1007\/3-540-53904-2_115"},{"key":"5_CR40","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 Lecture Notes in Computer Science, pages 371\u2013389. Springer-Verlag, 1992.","DOI":"10.1007\/3-540-55253-7_22"},{"key":"5_CR41","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 Lecture Notes in Computer Science, pages 477\u2013491. Springer-Verlag, 1992.","DOI":"10.1007\/3-540-55602-8_186"},{"key":"5_CR42","doi-asserted-by":"crossref","unstructured":"R. Nieuwenhuis and A. Rubio. AC-superposition with constraints: no AC-unifiers needed. In A. Bundy, editor, Proceedings of CADE-12, volume 814 of Lecture Notes in Computer Science, pages 545\u2013559. Springer-Verlag, 1994.","DOI":"10.1007\/3-540-58156-1_40"},{"key":"5_CR43","unstructured":"J. Pedersen. Confluence methods and the word problem in universal algebra. PhD thesis, Emory University, 1984."},{"key":"5_CR44","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. Journal of the ACM, 28:233\u2013264, 1981.","journal-title":"Journal of the ACM"},{"key":"5_CR45","doi-asserted-by":"crossref","unstructured":"G. E. Peterson. Complete sets of reductions with constraints. In M. E. Stickel, editor, Proceedings 10th International Conference on Automated Deduction, Kaiserslautern (Germany), volume 449 of Lecture Notes in Computer Science, pages 381\u2013395. Springer-Verlag, 1990.","DOI":"10.1007\/3-540-52885-7_101"},{"key":"5_CR46","doi-asserted-by":"crossref","unstructured":"A. Rubio and R. Nieuwenhuis. A precedence-based total ac-compatible ordering. In C. Kirchner, editor, Proceedings 5th Conference on Rewriting Techniques and Applications, Montreal (Canada), volume 690 of Lecture Notes in Computer Science, pages 374\u2013388. Springer-Verlag, 1993.","DOI":"10.1007\/3-540-56868-9_28"},{"key":"5_CR47","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1007\/BF02573590","volume":"25","author":"J. Siekmann","year":"1982","unstructured":"J. Siekmann and P. Szab\u00f3. A noetherian and confluent rewrite system for idempotent semigroups. Semigroup Forum, 25:83\u2013110, 1982.","journal-title":"Semigroup Forum"},{"key":"5_CR48","volume-title":"PhD thesis","author":"G. Smolka","year":"1989","unstructured":"G. Smolka. Logic Programming over Polymorphically Order-Sorted Types. PhD thesis, FB Informatik, Universit\u00e4t Kaiserslautern, Germany, 1989."},{"key":"5_CR49","doi-asserted-by":"crossref","unstructured":"M. E. Stickel. A case study of theorem proving by the Knuth-Bendix method: Discovering that x 3=x implies ring commutativity. In R. Shostak, editor, Proceedings 7th International Conference on Automated Deduction, Napa Valley (Calif., USA), volume 170 of Lecture Notes in Computer Science, pages 248\u2013258. Springer-Verlag, 1984.","DOI":"10.1007\/BFb0047125"},{"key":"5_CR50","volume-title":"Internal Report ANL-81-6","author":"R. L. Veroff","year":"1981","unstructured":"R. L. Veroff. Canonicalization and demodulation. Internal Report ANL-81-6, Argonne National Laboratory, Argonne, IL, 1981."},{"key":"5_CR51","doi-asserted-by":"crossref","unstructured":"L. Vigneron. Associative-commutative deduction with constraints. In A. Bundy, editor, Proceedings of CADE-12, volume 814 of Lecture Notes in Computer Science, pages 530\u2013544. Springer-Verlag, 1994.","DOI":"10.1007\/3-540-58156-1_39"},{"key":"5_CR52","volume-title":"Automated Reasoning: 33 basic research problems","author":"L. Wos","year":"1988","unstructured":"L. Wos. Automated Reasoning: 33 basic research problems. Prentice-Hall, Englewood Cliffs, NJ, 1988."}],"container-title":["Term Rewriting","Lecture Notes in Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-59340-3_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:26:58Z","timestamp":1605648418000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-59340-3_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540593409","9783540492375"],"references-count":52,"URL":"http:\/\/dx.doi.org\/10.1007\/3-540-59340-3_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"published":{"date-parts":[[1995]]}}}