{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T04:10:51Z","timestamp":1649131851454},"publisher-location":"Berlin, Heidelberg","reference-count":68,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540578673","type":"print"},{"value":"9783540483618","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-57867-6_2","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T13:32:35Z","timestamp":1330263155000},"page":"30-52","source":"Crossref","is-referenced-by-count":0,"title":["Rewriting techniques for software engineering"],"prefix":"10.1007","author":[{"given":"Jean-Pierre","family":"Jouannaud","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,27]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Leo Bachmair. Proof by consistency in equational theories. In Proc. 3rd IEEE Symp. Logic in Computer Science, Edinburgh, July 1988.","DOI":"10.1109\/LICS.1988.5122"},{"key":"2_CR2","doi-asserted-by":"crossref","volume-title":"Canonical Equational Proofs","author":"L. Bachmair","year":"1991","unstructured":"Leo Bachmair. Canonical Equational Proofs. Birkh\u00e4user, Boston, 1991.","DOI":"10.1007\/978-1-4684-7118-2"},{"issue":"1","key":"2_CR3","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S0747-7171(88)80018-X","volume":"6","author":"L. Bachmair","year":"1988","unstructured":"Leo Bachmair and Nachum Dershowitz. Critical pair criteria for completion. Journal of Symbolic Computation, 6(1):1\u201318, 1988.","journal-title":"Journal of Symbolic Computation"},{"key":"2_CR4","unstructured":"Leo Bachmair, Nachum Dershowitz, and Jieh Hsiang. Orderings for equational proofs. In Proc. 1st IEEE Symp. Logic in Computer Science, Cambridge, Mass., pages 346\u2013357, June 1986."},{"key":"2_CR5","volume-title":"LNCS 607","author":"L. Bachmair","year":"1992","unstructured":"Leo Bachmair, Harald Ganzinger, Christopher Lynch, and Wayne Snyder. Basic paramodulation and superposition. In Deepak Kapur, editor, Proc. 11th Int. Conf. on Automated Deduction, Saratoga Springs, NY, LNCS 607. Springer-Verlag, June 1992."},{"key":"2_CR6","unstructured":"Franco Barbanera and Maribel Fern\u00e1ndez. Combining first and higher order rewrite systems with type assignment systems. In Proceedings of the International Conference on Typed Lambda Calculi and Applications, Utrecht, Holland, 1993."},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"Franco Barbanera and Maribel Fern\u00e1ndez. Modularity of termination and confluence in combinations of rewrite systems with \u03bb\u03c9. In Proceedings of the 20th International Colloquium on Automata, Languages, and Programming, 1993.","DOI":"10.1007\/3-540-56939-1_110"},{"key":"2_CR8","unstructured":"Val Breazu-Tannen and Jean Gallier. Polymorphic rewriting conserves algebraic confluence. Information and Computation. to appear."},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"A-C. Caron, J.-L. Coquid\u00e9, and M. Dauchet. Encompassment properties and automata with constraints. In Proc. RTA 93, 1993.","DOI":"10.1007\/3-540-56868-9_25"},{"key":"2_CR10","volume-title":"Th\u00e8se de Doctorat","author":"H. Comon","year":"1988","unstructured":"Hubert Comon. Unification et disunification: Th\u00e9orie et applications. Th\u00e8se de Doctorat, Institut National Polytechnique de Grenoble, France, 1988."},{"key":"2_CR11","first-page":"76","volume-title":"LNCS 355","author":"H. Comon","year":"1989","unstructured":"Hubert Comon. Inductive proofs by specifications transformation. In Proc. 3rd Rewriting Techniques and Applications, Chapel Hill, LNCS 355, pages 76\u201391. Springer-Verlag, April 1989."},{"issue":"4","key":"2_CR12","doi-asserted-by":"crossref","first-page":"387","DOI":"10.1142\/S0129054190000278","volume":"1","author":"H. Comon","year":"1990","unstructured":"Hubert Comon. Solving symbolic ordering constraints. International Journal of Foundations of Computer Science, 1(4):387\u2013411, 1990.","journal-title":"International Journal of Foundations of Computer Science"},{"key":"2_CR13","unstructured":"Hubert Comon. Disunification: a survey. In Jean-Louis Lassez and Gordon Plotkin, editors, Computational Logic: Essays in Honor of Alan Robinson. MIT Press, 1991."},{"key":"2_CR14","volume-title":"LNCS 623","author":"H. Comon","year":"1992","unstructured":"Hubert Comon. Completion of rewrite systems with membership constraints. In W. Kuich, editor, Proc. 19th Int. Coll. on Automata, Languages and Programming, LNCS 623, Vienna, 1992. Springer-Verlag. An extended version is available as LRI Research Report number 699, Sept. 1991."},{"key":"2_CR15","unstructured":"Nachum Dershowitz. Applications of the Knuth-Bendix completion procedure. In Proceedings of the Seminaire d'Informatique Theorique, pages 95\u2013111, Paris, France, December 1982."},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"Nachum Dershowitz. A taste of rewrite systems. In Proc. Functional Programming, Concurrency, Simulation and Automated Reasonning, 1993.","DOI":"10.1007\/3-540-56883-2_11"},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"Nachum Dershowitz. Trees, ordinals and termination. In Proc. CAAP 93, LNCS 668, 1993.","DOI":"10.1007\/3-540-56610-4_68"},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"Nachum Dershowitz and Charles Hoot. Topics in termination. In Proc. 5th Rewriting Techniques and Applications, Montr\u00e9al, LNCS 690, 1993.","DOI":"10.1007\/3-540-56868-9_16"},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 243\u2013309. North-Holland, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"Nachum Dershowitz, St\u00e9phane Kaplan, and David A. Plaisted. Infinite normal forms. In Proc. 16th Int. Coll. on Automata, Languages and Programming, LNCS 372, pages 249\u2013262, Stresa, Italy, July 1989. European Association of Theoretical Computer Science.","DOI":"10.1007\/BFb0035765"},{"key":"2_CR21","volume-title":"Th\u00e8se de Doctorat","author":"H. Devie","year":"1991","unstructured":"Herv\u00e9 Devie. Une approche alg\u00e9brique de la r\u00e9\u00e9criture de preuves \u00e9quationnelles et son application \u00e0 la d\u00e9rivation de proc\u00e9dures de compl\u00e9tion. Th\u00e8se de Doctorat, Universit\u00e9 de Paris-Sud, France, Octobre 1991."},{"key":"2_CR22","unstructured":"Volker Diekert. On the Knuth-Bendix completion for concurrent processes. Universit\u00e4t M\u00fcnchen."},{"key":"2_CR23","unstructured":"K. Drosten. On termination in combined term rewriting systems:theoretical back-ground and application to prototyping parametric algebraic specifications. TU Braunshweig."},{"key":"2_CR24","unstructured":"M. Fay. First-order unification in an equational theory. In Proc. 4th Workshop on Automated Deduction, Austin, Texas, pages 161\u2013167, 1979."},{"key":"2_CR25","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF01189020","volume":"3","author":"M. Fern\u00e1ndez","year":"1992","unstructured":"Maribel Fern\u00e1ndez. Narrowing based procedures for equational disunification. Applicable Algebra in Engineering Communication and Computing, 3:1\u201326, 1992.","journal-title":"Applicable Algebra in Engineering Communication and Computing"},{"key":"2_CR26","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1016\/S0747-7171(89)80069-0","volume":"8","author":"L. Fribourg","year":"1989","unstructured":"Laurent Fribourg. A strong restriction of the inductive completion procedure. Journal of Symbolic Computation, 8:253\u2013276, 1989.","journal-title":"Journal of Symbolic Computation"},{"key":"2_CR27","doi-asserted-by":"crossref","unstructured":"J. A. Goguen. How to prove inductive hypothesis without induction. In Proc. 5th Conf. on Automated Deduction, Les Arcs, France, LNCS 87, July 1980.","DOI":"10.1007\/3-540-10009-1_27"},{"key":"2_CR28","unstructured":"J. A. Goguen, T. Winkler, Jos\u00e9 Meseguer, K. Futatsugi, and Jean-Pierre Jouannaud. Applications of Algebraic Specifications Using OBJ, chapter Introducing OBJ. Cambridge University Press, 1991. D. Coleman, R. Gallimore and J. Goguen eds."},{"key":"2_CR29","unstructured":"G. Gonthier, J.-J. L\u00e9vy, and P.-A. Mellies. An abstract standardisation theorem. In Proc. 7th IEEE Symp. on Logic in Computer Science, Santa Cruz, CA, 1992."},{"key":"2_CR30","doi-asserted-by":"crossref","unstructured":"Jieh Hsiang and Micha\u00ebl Rusinowitch. On word problems in equational theories. In Proc. in 14th ICALP Karlsruhe, July 1987.","DOI":"10.1007\/3-540-18088-5_6"},{"issue":"4","key":"2_CR31","doi-asserted-by":"crossref","first-page":"797","DOI":"10.1145\/322217.322230","volume":"27","author":"G. Huet","year":"1980","unstructured":"G\u00e9rard 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":"2_CR32","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1016\/0022-0000(81)90002-7","volume":"23","author":"G. Huet","year":"1981","unstructured":"G\u00e9rard Huet. A complete proof of correctness of the Knuth-Bendix completion algorithm. Journal of Computer and System Sciences, 23:11\u201321, 1981.","journal-title":"Journal of Computer and System Sciences"},{"key":"2_CR33","doi-asserted-by":"crossref","unstructured":"G\u00e9rard Huet and J.-M. Hullot. Proofs by induction in equational theories with constructors. Journal of Computer and System Sciences, 25(2), 1982.","DOI":"10.1016\/0022-0000(82)90006-X"},{"key":"2_CR34","unstructured":"G\u00e9rard Huet. and Jean-Jacques L\u00e9vy. Computations in orthogonal term rewriting systems. In Gordon Plotkin and Jean-Louis Lassez, editors, Computational Logic: essays in Honour of Alan Robinson. MIT Press, 1990."},{"key":"2_CR35","doi-asserted-by":"crossref","unstructured":"J.-M. Hullot. Canonical forms and unification. In Proc. 5th Conf. on Automated Deduction, Les Arcs, France, LNCS 87. Springer-Verlag, July 1980.","DOI":"10.21236\/ADA087640"},{"key":"2_CR36","unstructured":"Jean-Pierre Jouannaud and Claude Kirchner. Solving equations in abstract algebras: A rule-based survey of unification. In Jean-Louis Lassez and Gordon Plotkin, editors, Computational Logic: Essays in Honor of Alan Robinson. MIT-Press, 1991."},{"issue":"4","key":"2_CR37","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 on Computing, 15(4):1155\u20131194, 1986.","journal-title":"SIAM Journal on Computing"},{"key":"2_CR38","doi-asserted-by":"crossref","unstructured":"Jean-Pierre Jouannaud and Emmanuel Kounalis. Automatic proofs by induction in theories without constructors. Information and Computation, 82(1), July 1989.","DOI":"10.1016\/0890-5401(89)90062-X"},{"key":"2_CR39","unstructured":"Jean-Pierre Jouannaud and Mitsuhiro Okada. Executable higher-order algebraic specification languages. In Proc. 6th IEEE Symp. Logic in Computer Science, Amsterdam, pages 350\u2013361, 1991."},{"key":"2_CR40","doi-asserted-by":"crossref","unstructured":"Jean-Pierre Jouannaud and Mitsuhiro Okada. Satisfiability of systems of ordinal notations with the subterm property is decidable. In Proc. 18th Int. Coll. on Automata, Languages and Programming, Madrid, LNCS 510, 1991.","DOI":"10.1007\/3-540-54233-7_155"},{"issue":"4","key":"2_CR41","doi-asserted-by":"crossref","first-page":"395","DOI":"10.1007\/BF00292110","volume":"24","author":"D. Kapur","year":"1987","unstructured":"Deepak Kapur, Paliath Narendran, and Hantao Zhang. On sufficient completeness and related properties of term rewriting systems. Acta Informatics, 24(4):395\u2013415, 1987.","journal-title":"Acta Informatics"},{"key":"2_CR42","doi-asserted-by":"crossref","unstructured":"J. R. Kennaway, J. W. Klop, M. R. Sleep, and F. J. de Vries. Transfinite reductions in orthogonal term rewriting systems. In Proc. 4th Rewriting Techniques and Applications, Como, LNCS 488, 1991.","DOI":"10.1007\/3-540-53904-2_81"},{"key":"2_CR43","volume-title":"Technical report","author":"J. W. Klop","year":"1989","unstructured":"Jan Willem Klop and Aart Middeldorp. Sequenliality in orthogonal term rewriting systems. Technical report, CWI, Amsterdam, 1989."},{"key":"2_CR44","doi-asserted-by":"crossref","unstructured":"Donald E. Knuth and Peter B. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263\u2013297. Pergamon Press, 1970.","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"2_CR45","series-title":"Information and Computation","volume-title":"Research Report 92-R-062","author":"G. Kucherov","year":"1992","unstructured":"G. Kucherov and M. Tajine. Decidability of regularity and related properties of ground normal form languages. Research Report 92-R-062, CRIN, Nancy, France, 1992. To appear in Information and Computation."},{"key":"2_CR46","unstructured":"Mahahito Kurihara and Azuma Ohuchi. Non-copying term rewriting and modularity of termination. Hokkaido University."},{"key":"2_CR47","doi-asserted-by":"crossref","unstructured":"Yves Lafont. Penrose diagrams and 2-dimensional rewriting, October 1991. extended abstract.","DOI":"10.1017\/CBO9780511525902.011"},{"key":"2_CR48","volume-title":"Th\u00e8se de Doctorat","author":"C. March\u00e9","year":"1993","unstructured":"Claude March\u00e9. R\u00e9\u00e9criture modulo une th\u00e9orie pr\u00e9sent\u00e9e par un syst\u00e8me convergent et d\u00e9cidabilit\u00e9 des probl\u00e8mes du mot dans certains classes de th\u00e9ories \u00e9quationnelles. Th\u00e8se de Doctorat, Universit\u00e9 de Paris-Sud, France, 1993."},{"key":"2_CR49","doi-asserted-by":"crossref","unstructured":"Jos\u00e9 Meseguer. General logics. Technical Report SRI-CSL-89-05, SRI International, March 1989. Proc. Logic Colloquium'87.","DOI":"10.1016\/S0049-237X(08)70132-0"},{"key":"2_CR50","doi-asserted-by":"crossref","unstructured":"Jos\u00e9 Meseguer. Conditional rewriting logic as a unified model of concurrency. Technical Report SRI-CSL-91-05, SRI International, February 1991. TCS 96 (1992) 73\u2013155.","DOI":"10.1016\/0304-3975(92)90182-F"},{"issue":"1","key":"2_CR51","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1016\/0020-0190(83)90009-1","volume":"16","author":"Y. M\u00e9tivier","year":"1983","unstructured":"Y. M\u00e9tivier. About the rewriting systems produced by the knuth-bendix completion algorithm. Information Processing Letters, 16(1):31\u201334, 1983.","journal-title":"Information Processing Letters"},{"key":"2_CR52","first-page":"263","volume-title":"LNCS 355","author":"A. Middeldorp","year":"1989","unstructured":"A. Middeldorp. Modular aspects of properties of term rewriting systems related to normal forms. In Proc. 3rd Rewriting Techniques and Applications, Chapel Hill, LNCS 355, pages 263\u2013277. Springer-Verlag, 1989."},{"key":"2_CR53","doi-asserted-by":"crossref","unstructured":"A. Middeldorp and Y. Toyama. Completeness of combinations of constructor systems. In Proc. 4th Rewriting Techniques and Applications, Como, LNCS 488, 1991.","DOI":"10.1007\/3-540-53904-2_96"},{"key":"2_CR54","volume-title":"PhD thesis","author":"A. Middeldorp","year":"1990","unstructured":"Aart Middeldorp. Modular Properties of Term Rewriting Systems. PhD thesis, Free University of Amsterdam, Netherland, 1990."},{"key":"2_CR55","doi-asserted-by":"crossref","unstructured":"D. Musser. Proving inductive properties of abstract data types. In Proc. 7th ACM Symp. Principles of Programming Languages, Las Vegas, 1980.","DOI":"10.1145\/567446.567461"},{"issue":"2","key":"2_CR56","doi-asserted-by":"crossref","first-page":"223","DOI":"10.2307\/1968867","volume":"43","author":"M. H. A. A. Newman","year":"1942","unstructured":"M. H. A. Newman. On theories with a combinatorial definition of \u2018equivalence'. Ann. Math., 43(2):223\u2013243, 1942.","journal-title":"Ann. Math."},{"key":"2_CR57","volume-title":"Tech. report","author":"R. Nieuwenhuis","year":"1991","unstructured":"Robert Nieuwenhuis and Albert Rubio. Completion of first-order clauses by basic superposition with ordering constraints. Tech. report, Dept. L.S.I., Univ. Polit. Catalunya, 1991. To appear in Proc. 11th Conf. on Automated Deduction, Saratoga Springs, 1992."},{"key":"2_CR58","first-page":"371","volume-title":"LNCS 582","author":"Robert. Nieuwenhuis","year":"1992","unstructured":"Robert. Nieuwenhuis and Albert Rubio. Basic superposition is complete. In B. Krieg-Bruckner, editor, Proc. European Symp. on Programming, LNCS 582, pages 371\u2013389, Rennes, 1992. Springer-Verlag."},{"issue":"3\/4","key":"2_CR59","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1016\/S0747-7171(89)80014-8","volume":"7","author":"W. Nutt","year":"1989","unstructured":"W. Nutt, P. R\u00e9ty, and Gert Smolka. Basic narrowing revisited. Journal of Symbolic Computation, 7(3\/4):295\u2013318, 1989.","journal-title":"Journal of Symbolic Computation"},{"issue":"2","key":"2_CR60","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1145\/322248.322251","volume":"28","author":"Gerald E. E. Peterson","year":"1981","unstructured":"Gerald E. Peterson and Mark E. Stickel. Complete sets of reductions for some equational theories. Journal of the ACM, 28(2):233\u2013264, April 1981.","journal-title":"Journal of the ACM"},{"key":"2_CR61","doi-asserted-by":"crossref","first-page":"182","DOI":"10.1016\/S0019-9958(85)80005-X","volume":"65","author":"D. Plaisted","year":"1985","unstructured":"David Plaisted. Semantic confluence tests and completion methods. Information and Control, 65:182\u2013215, 1985.","journal-title":"Information and Control"},{"issue":"2\u20133","key":"2_CR62","doi-asserted-by":"crossref","first-page":"182","DOI":"10.1016\/S0019-9958(85)80005-X","volume":"65","author":"David A. A. Plaisted","year":"1985","unstructured":"David A. Plaisted. Semantic confluence tests and completion methods. Information and Control, 65(2\u20133):182\u2013215, May\/June 1985.","journal-title":"Information and Control"},{"key":"2_CR63","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1016\/0022-4049(87)90129-0","volume":"49","author":"C. C. Squier","year":"1987","unstructured":"C. C. Squier. Word problems and a homological finiteness condition for monoids. Journal of Pure and Applied Algebra, 49:201\u2013217, 1987.","journal-title":"Journal of Pure and Applied Algebra"},{"key":"2_CR64","doi-asserted-by":"crossref","unstructured":"W. Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, pages 134\u2013191. Elsevier, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"key":"2_CR65","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1016\/0020-0190(87)90122-0","volume":"25","author":"Y. Toyama","year":"1987","unstructured":"Y. Toyama. Counterexamples to termination for the direct sum of term rewriting systems. Information Processing Letters, 25:141\u2013143, April 1987.","journal-title":"Information Processing Letters"},{"issue":"1","key":"2_CR66","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1145\/7531.7534","volume":"34","author":"Y. Toyama","year":"1987","unstructured":"Y. Toyama. On the Church-Rosser property for the direct sum of term rewriting systems. Journal of the ACM, 34(1):128\u2013143, April 1987.","journal-title":"Journal of the ACM"},{"key":"2_CR67","volume-title":"Tech. Report. A-09\/90","author":"R. Treinen","year":"1990","unstructured":"Ralf Treinen. A new method for undecidability proofs of first order theories. Tech. Report. A-09\/90, Universit\u00e4t des Saarladandes, Saarbr\u00fccken, May 1990."},{"key":"2_CR68","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1016\/S0747-7171(08)80020-X","volume":"9","author":"H. Zhang","year":"1990","unstructured":"H. Zhang. Automated proof of ring commutativity problems by algebraic methods. Journal of Symbolic Computation, 9:423\u2013427, 1990.","journal-title":"Journal of Symbolic Computation"}],"container-title":["Recent Trends in Data Type Specification","Lecture Notes in Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-57867-6_2.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,31]],"date-time":"2021-12-31T05:48:10Z","timestamp":1640929690000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-57867-6_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540578673","9783540483618"],"references-count":68,"URL":"http:\/\/dx.doi.org\/10.1007\/3-540-57867-6_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"published":{"date-parts":[[1994]]}}}