{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T23:07:54Z","timestamp":1773702474066,"version":"3.50.1"},"reference-count":200,"publisher":"Elsevier","isbn-type":[{"value":"9780444508133","type":"print"}],"license":[{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1016\/b978-044450813-3\/50011-4","type":"book-chapter","created":{"date-parts":[[2007,6,11]],"date-time":"2007-06-11T13:04:11Z","timestamp":1181567051000},"page":"535-610","source":"Crossref","is-referenced-by-count":95,"title":["Rewriting"],"prefix":"10.1016","author":[{"given":"Nachum","family":"Dershowitz","sequence":"first","affiliation":[]},{"given":"David A.","family":"Plaisted","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/B978-044450813-3\/50011-4_bb0010","first-page":"79","article-title":"Automated proofs of the Moufang identities in alternative rings","volume":"6","author":"Anantharaman","year":"1990","journal-title":"J. Symbolic Computation"},{"issue":"4","key":"10.1016\/B978-044450813-3\/50011-4_bb0015","doi-asserted-by":"crossref","first-page":"865","DOI":"10.1137\/0213054","article-title":"Cylindrical algebraic decomposition. I. The basic algorithm","volume":"13","author":"Arnon","year":"1984","journal-title":"SIAM J. Comput."},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0020","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1016\/S0304-3975(99)00207-8","article-title":"Termination of term rewriting using dependency pairs","volume":"236","author":"Arts","year":"2000","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0025","series-title":"Formal Techniques in Artificial Intelligence: A Sourcebook","article-title":"Term rewriting and equational reasoning","author":"Avenhaus","year":"1989"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0030","series-title":"Formal Techniques in Artificial Intelligence: A Sourcebook","first-page":"1","article-title":"Term rewriting and equational reasoning","author":"Avenhaus","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0035","series-title":"Term Rewriting and All That","author":"Baader","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0040","first-page":"445","article-title":"Unification theory","volume":"Vol. I","author":"Baader","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0045","series-title":"Proceedings of the Eighth International Conference on Automated Deduction (Oxford, England)","first-page":"5","article-title":"Commutation, transformation, and termination","volume":"Vol. 230","author":"Bachmair","year":"1986"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0050","series-title":"Proceedings of the Second IEEE Symposium on Logic in Computer Science","first-page":"331","article-title":"Inference rules for rewrite-based first-order theorem proving","author":"Bachmair","year":"1987"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50011-4_rf0055","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S0747-7171(88)80018-X","article-title":"Critical pair criteria for completion","volume":"6","author":"Bachmair","year":"1988","journal-title":"J. Symbolic Computation"},{"issue":"2 & 3","key":"10.1016\/B978-044450813-3\/50011-4_bb0060","article-title":"Completion for rewriting modulo a congruence","volume":"67","author":"Bachmair","year":"1989","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50011-4_bb0065","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1145\/174652.174655","article-title":"Equational inference, canonical proofs, and proof orderings","volume":"41","author":"Bachmair","year":"1994","journal-title":"J. of the Association for Computing Machinery"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0070","series-title":"Resolution of Equations in Algebraic Structures, Vol. 2: Rewriting Techniques","first-page":"1","article-title":"Completion without failure","author":"Bachmair","year":"1989"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0075","first-page":"19","article-title":"Resolution theorem proving","volume":"Vol. I","author":"Bachmair","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0080","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1016\/S0747-7171(85)80019-5","article-title":"Termination orderings for associative-commutative rewriting systems","volume":"1","author":"Bachmair","year":"1985","journal-title":"J. Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0085","series-title":"Proceedings of the 3rd International Conference on rewriting techniques and applications","first-page":"29","article-title":"Complete sets of reductions modulo associativity, commutativity, and identity","author":"Baird","year":"1989"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0090","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1016\/0898-1221(81)90115-2","article-title":"New decision algorithms for finitely presented commutative semigroups","volume":"7","author":"Ballantyne","year":"1981","journal-title":"J. Computational Mathematics with Applications"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0095","article-title":"Gr\u00f6bner Bases: A Computational Approach to Commutative Algebra","volume":"Vol. 141","author":"Becker","year":"1993"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50011-4_bb0100","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1007\/BF01810293","article-title":"Termination by completion","volume":"1","author":"Bellegarde","year":"1990","journal-title":"Applied Algebra on Engineering, Communication and Computer Science"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50011-4_bb0105","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1016\/0167-6423(87)90030-X","article-title":"Termination of rewriting systems by polynomial interpretations and its implementation","volume":"9","author":"Ben Cherifa","year":"1987","journal-title":"Science of Computer Programming"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0110","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-18598-4","article-title":"Systems of Reductions","author":"Benninghofen","year":"1987"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0115","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1016\/0022-0000(86)90033-4","article-title":"Conditional rewrite rules: Confluency and termination","volume":"32","author":"Bergstra","year":"1986","journal-title":"J. of Computer and System Sciences"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0120","series-title":"Proceedings of the Third International Conference on Rewriting Techniques and Applications (Chapel Hill, NC)","first-page":"45","article-title":"Completion-time optimization of rewrite-time goal solving","author":"Bertling","year":"1989"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0125","series-title":"Proceedings of the Cambridge Philosophical Society","first-page":"433","article-title":"On the structure of abstract algebras","author":"Birkhoff","year":"1935"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0130","series-title":"Proc. 14th Annual IEEE Symposium on Logic in Computer Science (Trento, Italy)","first-page":"225","article-title":"Paramodulation with nonmonotonic orderings","author":"Bofill","year":"1999"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0135","series-title":"String-Rewriting Systems","author":"Book","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0140","series-title":"Proceedings of the International Conference on Automated Deduction","first-page":"346","article-title":"Complete monotonic semantic path orderings","author":"Borralleras","year":"2000"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0145","series-title":"Proceedings of the Fourth Workshop on Automated Deduction","article-title":"Completeness of conditional reductions","author":"Brand","year":"1979"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0150","unstructured":"Breazu-Tannen V. and Gallier J. [to appear], \u2018Polymorphic rewriting conserves algebraic strong normalization\u2019, Theoretical Computer Science."},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0155","article-title":"A Structured Design-Method for Specialized Proof Procedures","author":"Brown","year":"1975","journal-title":"PhD thesis, California Institute of Technology, Pasadena, CA"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50011-4_bb0160","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1142\/S0218196791000249","article-title":"Term rewrite rules for finite fields","volume":"1","author":"Burris","year":"1991","journal-title":"International Journal of Algebra and Computation"},{"key":"10.1016\/B978-044450813-3\/50011-4_rf0160","series-title":"Experiments with computer implementations of procedures which often derive decision algorithms for the word problem in abstract algebras, Memo MTP-7","author":"Butler","year":"1980"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0170","series-title":"Proceedings of the Twenty First Conference on Foundations of Computer Science","first-page":"108","article-title":"An improved algorithm for computing with equations","author":"Chew","year":"1980"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0175","series-title":"Proceedings of the 13th Annual Symposium on the Theory of Computing","first-page":"7","article-title":"Unique normal forms in term rewriting systems with repeated variables","author":"Chew","year":"1981"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0180","series-title":"Proceedings of the Third International Conference on Rewriting Techniques and Applications (Chapel Hill, NC)","first-page":"551","article-title":"Fast Knuth-Bendix completion: Summary","author":"Christian","year":"1989"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0185","series-title":"Light LOP, Rapport de Recheerche 99-R-138","author":"Cichon","year":"1999"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0190","series-title":"Frontiers of Combining Systems 2","first-page":"95","article-title":"Combining higher-order and first-order computation using \u03c1-calculus: Towards a semantics of ELAN","author":"Cirstea","year":"1999"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0195","series-title":"Proceedings of the Fifth Annual Symposium on Logic in Computer Science","first-page":"62","article-title":"Solving inequations in term algebras (Preliminary version)","author":"Comon","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0200","first-page":"913","article-title":"Inductionless induction","volume":"Vol. I","author":"Comon","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0205","series-title":"Proc. of the 13th Annual IEEE Symposium on Logic in Computer Science","first-page":"276","article-title":"Decision problems in ordered rewriting","author":"Comon","year":"1998"},{"issue":"1-2","key":"10.1016\/B978-044450813-3\/50011-4_bb0210","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1016\/S0304-3975(96)00049-7","article-title":"The first-order theory of lexicographic path orderings is undecidable","volume":"176","author":"Comon","year":"1997","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50011-4_bb0215","doi-asserted-by":"crossref","first-page":"409","DOI":"10.1016\/0304-3975(92)90022-8","article-title":"Simulation of Turing machines by a regular rewrite rule","volume":"103","author":"Dauchet","year":"1992","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0220","series-title":"Proceedings of the Second Symposium on Logic in Computer Science","first-page":"353","article-title":"Decidability of the confluence of ground term rewriting systems","author":"Dauchet","year":"1987"},{"issue":"5","key":"10.1016\/B978-044450813-3\/50011-4_bb0225","doi-asserted-by":"crossref","first-page":"212","DOI":"10.1016\/0020-0190(79)90071-1","article-title":"A note on simplification orderings","volume":"9","author":"Dershowitz","year":"1979","journal-title":"Information Processing Letters"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0230","series-title":"Proceedings of the Eighth International Colloquium on Automata, Languages and Programming (Acre, Israel)","first-page":"448","article-title":"Termination of linear rewriting systems","author":"Dershowitz","year":"1981"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50011-4_bb0235","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","article-title":"Orderings for term-rewriting systems","volume":"17","author":"Dershowitz","year":"1982","journal-title":"Theoretical Computer Science"},{"issue":"2\/3","key":"10.1016\/B978-044450813-3\/50011-4_bb0240","doi-asserted-by":"crossref","first-page":"122","DOI":"10.1016\/S0019-9958(85)80003-6","article-title":"Computing with rewrite systems","volume":"64","author":"Dershowitz","year":"1985","journal-title":"Information and Control"},{"issue":"1&2","key":"10.1016\/B978-044450813-3\/50011-4_bb0245","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/S0747-7171(87)80022-6","article-title":"Termination of rewriting","volume":"3","author":"Dershowitz","year":"1987","journal-title":"J. Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0250","series-title":"Proceedings of the Eighteenth International Colloquium on Automata, Languages and Programming (Madrid, Spain)","first-page":"267","article-title":"Canonical sets of Horn clauses","author":"Dershowitz","year":"1991"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0255","series-title":"Proceedings of the Twelfth International Joint Conference on Artificial Intelligence","first-page":"118","article-title":"Ordering-based strategies for Horn clauses","author":"Dershowitz","year":"1991"},{"key":"10.1016\/B978-044450813-3\/50011-4_rf0255","series-title":"Proceedings of the Fourth International Workshop on Conditional and Typed Rewriting Systems (Jerusalem, Israel, July 1994)","first-page":"89","article-title":"Hierarchical termination","author":"Dershowitz","year":"1995"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50011-4_bb0265","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1016\/0304-3975(94)00275-4","article-title":"Natural termination","volume":"142","author":"Dershowitz","year":"1995","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0270","series-title":"Proceedings of the Eighth International Joint Conference on Artificial Intelligence","first-page":"940","article-title":"Associative-commutative rewriting","author":"Dershowitz","year":"1983"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0275","series-title":"Using Boolean rings and simplification to test satisfiability","author":"Dershowitz","year":"2000"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0280","series-title":"\u2018Handbook of Theoretical Computer Science\u2019, Vol. B: Formal Methods and Semantics","first-page":"243","article-title":"Rewrite systems","author":"Dershowitz","year":"1990"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50011-4_bb0285","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1016\/0304-3975(91)90040-9","article-title":"Rewrite, rewrite, rewrite, rewrite, rewrite,\u2026,","volume":"83","author":"Drshowitz","year":"1991","journal-title":"Theoretical Computer Science"},{"issue":"8","key":"10.1016\/B978-044450813-3\/50011-4_bb0290","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1145\/359138.359142","article-title":"Proving termination with multiset orderings","volume":"22","author":"Dershowitz","year":"1979","journal-title":"Communications of the ACM"},{"issue":"4","key":"10.1016\/B978-044450813-3\/50011-4_bb0295","doi-asserted-by":"crossref","first-page":"629","DOI":"10.1137\/0217039","article-title":"Existence, uniqueness, and construction of rewrite systems","volume":"17","author":"Dershowitz","year":"1988","journal-title":"SIAM J. on Computing"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0300","series-title":"Proceedings of the Third IEEE Symposium on Logic in Computer Science","first-page":"104","article-title":"Proof-theoretic techniques and the theory of rewriting","author":"Dershowitz","year":"1988"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0305","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1016\/0304-3975(90)90064-O","article-title":"A rationale for conditional equational programming","volume":"75","author":"Dershowitz","year":"1990","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0310","series-title":"Proceedings of the First International Workshop on Conditional Term Rewriting Systems (Orsay, France)","first-page":"31","article-title":"Confluence of conditional rewrite systems","author":"Dershowitz","year":"1987"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0315","series-title":"Proceedings of the Ninth Conference on Automated Deduction (Argonne, IL)","first-page":"538","article-title":"Canonical conditional rewrite systems","author":"Dershowitz","year":"1988"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0320","series-title":"Machine Intelligence 11: The logic and acquisition of knowledge","first-page":"21","article-title":"Equational programming","author":"Dershowitz","year":"1988"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0325","doi-asserted-by":"crossref","first-page":"467","DOI":"10.1016\/S0747-7171(06)80002-7","article-title":"Deductive and inductive synthesis of equational programs","volume":"15","author":"Dershowitz","year":"1993","journal-title":"J. Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0330","series-title":"Proceedings of the First International Conference on Rewriting Techniques and Applications (Dijon, France)","first-page":"255","article-title":"A procedure for automatically proving the termination of a set of rewrite rules","author":"Detlefs","year":"1985"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0335","series-title":"Proceedings of the Second International Workshop on Conditional and Typed Rewriting Systems (Montreal, Canada)","article-title":"When ordered completion fails","volume":"Vol. 516","author":"Devie","year":"1990"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50011-4_bb0340","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1007\/BF01237233","article-title":"Automating the Knuth Bendix ordering","volume":"28","author":"Dick","year":"1990","journal-title":"Acta Informatica"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0345","series-title":"Higher-order unification via explicit substitutions","author":"Dowes","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0350","unstructured":"Edelson R. [1990]. Private Communication."},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0355","doi-asserted-by":"crossref","first-page":"637","DOI":"10.1017\/S0305004100027092","article-title":"On multiplicative systems defined by generators and relations, I","volume":"47","author":"Evans","year":"1951","journal-title":"Proceedings of the Cambridge Philosophical Society"},{"key":"10.1016\/B978-044450813-3\/50011-4_rf0350","series-title":"Proceedings of the Fifth Conference on Rewriting Techniques and Applications","first-page":"213","article-title":"Total termination of term rewriting","volume":"Vol.690","author":"Ferreira","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0365","series-title":"Proceedings of an International Workshop on Algebraic and Logic Programming","first-page":"146","article-title":"Rewrite rule systems for modal propositional logic","author":"Foret","year":"1988"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0370","series-title":"Proceedings of the Symposium on Logic Programming","first-page":"172","article-title":"Slog: A logic programming language interpreter based on clausal superposition and rewriting","author":"Fribourg","year":"1985"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50011-4_bb0375","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1016\/0168-0072(91)90022-E","article-title":"What's so special about Kruskal's Theorem and the ordinal \u04130. A survey of some results in proof theory","volume":"53","author":"Gallier","year":"1991","journal-title":"Annals of Pure and Applied Logic"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0380","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1016\/S0747-7171(08)80132-0","article-title":"A completion procedure for conditional equations","volume":"11","author":"Ganzinger","year":"1991","journal-title":"Journal of Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0385","series-title":"Proceedings 22nd International Colloquium on Trees in Algebra and Programming (Lille, France)","first-page":"249","article-title":"Termination proofs using GPO ordering constraints","volume":"Vol. 1214","author":"Genet","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0390","article-title":"Overlap closures and termination of term rewriting systems","author":"Geupel","year":"1989","journal-title":"Report MIP-8922, Universit\u00e4t Passau, Passau, West Germany"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0395","series-title":"Proceedings of the Sixth International Conference on Rewriting Techniques and Applications (Kaiserslautern, Germany)","first-page":"426","article-title":"Generating polynomial orderings for termination proofs","volume":"vol. 279","author":"Giesl","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0400","series-title":"Presented at the First International Workshop on Conditional Term Rewriting Systems","article-title":"A completeness result for conditional narrowing","author":"Giovannetti","year":"1987"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0405","series-title":"Proceedings of Graph Reduction Workshop (Santa Fe, NM)","first-page":"53","article-title":"Concurrent term rewriting as a model of computation","volume":"vol. 279","author":"Goguen","year":"1987"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0410","series-title":"Logic Programming: Functions, Relations, and Equations","first-page":"295","article-title":"Eqlog: Equality, types, and generic modules for logic programming","author":"Goguen","year":"1986"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0415","doi-asserted-by":"crossref","first-page":"3","DOI":"10.3233\/FI-1995-24121","article-title":"Abstract relations between restricted termination and confluence properties of rewrite systems","volume":"24","author":"Gramlich","year":"1995","journal-title":"Fundamenta Informaticae"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0420","series-title":"Proceedings of the International Conference on Rewriting Techniques and Applications","first-page":"245","article-title":"Confluence of terminating conditional rewrite systems revisited","volume":"vol. 1103","author":"Gramlich","year":"1996"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50011-4_bb0425","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1137\/0212012","article-title":"On proving uniform termination and restricted termination of rewriting systems","volume":"12","author":"Guttag","year":"1983","journal-title":"SIAM J. on Computing"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0430","doi-asserted-by":"crossref","first-page":"583","DOI":"10.1016\/0743-1066(94)90034-5","article-title":"The integration of functions into logic programming: From theory to practice","volume":"19&20","author":"Hanus","year":"1994","journal-title":"J. Logic Programming"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0435","series-title":"Proc. Twelfth International Conference on Logic Programming","first-page":"665","article-title":"On extra variables in (equational) logic programming","author":"Hanus","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0440","series-title":"Proceedings of the London Mathematical Society (3)","first-page":"326","article-title":"Ordering by divisibility in abstract algebras","author":"Higman","year":"1952"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0445","doi-asserted-by":"crossref","first-page":"215","DOI":"10.5486\/PMD.1952.2.3-4.10","article-title":"Groups as groupoids with one law","volume":"2","author":"Higman","year":"1952","journal-title":"Publ. Math. Debrecen"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0450","article-title":"The Church-Rosser Property and a Result in Combinatory Logic","author":"Hindley","year":"1964","journal-title":"PhD thesis, University of Newcastle-upon-Tyne"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50011-4_bb0455","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1016\/0304-3975(92)90289-R","article-title":"Termination proofs by multiset path orderings imply primitive recursive derivation lengths","volume":"105","author":"Hofbauer","year":"1992","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/B978-044450813-3\/50011-4_rf0450","series-title":"Proceedings of the 3rd International Conference on rewriting techniques and applications","first-page":"167","article-title":"Termination proofs and the length of derivations (preliminary version)","volume":"Vol. 355","author":"Hofbauer","year":"1989"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50011-4_bb0465","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1145\/357153.357158","article-title":"Programming with equations","volume":"4","author":"Hoffmann","year":"1982","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0470","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1016\/0004-3702(85)90074-8","article-title":"Refutational theorem proving using term-rewriting systems","volume":"25","author":"Hsiang","year":"1985","journal-title":"Artificial Intelligence"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0475","series-title":"Proceedings of the Tenth International Colloquium on Automata, Languages and Programming (Barcelona, Spain)","first-page":"331","article-title":"Rewrite methods for clausal and non-clausal theorem proving","volume":"Vol. 35","author":"Hsiang","year":"1983"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0480","series-title":"Satisfiability Problem: Theory and Applications","first-page":"587","article-title":"Some fundamental properties of Boolean ring normal forms","volume":"Vol. 267","author":"Hsiang","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0485","series-title":"Proceedings of the Fourteenth EATCS International Conference on Automata, Languages and Programming (Karlsruhe, West Germany)","first-page":"54","article-title":"On word problems in equational theories","volume":"Vol. 242","author":"Hsiang","year":"1987"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50011-4_bb0490","doi-asserted-by":"crossref","first-page":"559","DOI":"10.1145\/116825.116833","article-title":"Proving refutational completeness of theorem proving strategies. The transfinite semantic tree method","volume":"38","author":"Hsiang","year":"1991","journal-title":"J. of the Association for Computing Machinery"},{"issue":"4","key":"10.1016\/B978-044450813-3\/50011-4_bb0495","doi-asserted-by":"crossref","first-page":"797","DOI":"10.1145\/322217.322230","article-title":"Confluent reductions: Abstract properties and applications to term rewriting systems","volume":"27","author":"Huet","year":"1980","journal-title":"J. of the Association for Computing Machinery"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50011-4_bb0500","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1016\/0022-0000(81)90002-7","article-title":"A complete proof of correctness of the Knuth-Bendix completion algorithm","volume":"23","author":"Huet","year":"1981","journal-title":"J. Computer and System Sciences"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0505","series-title":"Proceedings of the LITP Spring School on Combinators and Functional Programming Languages","first-page":"123","article-title":"Cartesian closed categories and Lambda-calculus","author":"Huet","year":"1985"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0510","series-title":"On the uniform halting problem for term rewriting systems, Rapport laboria 283","author":"Huet","year":"1978"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0515","series-title":"Computational Logic: Essays in Honor of Alan Robinson","first-page":"395","article-title":"Computations in orthogonal rewriting systems, I and II","author":"Huet","year":"1991"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0520","doi-asserted-by":"crossref","DOI":"10.21236\/ADA087641","article-title":"A catalogue of canonical term rewriting systems","author":"Hullot","year":"1980"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0525","doi-asserted-by":"crossref","first-page":"1155","DOI":"10.1137\/0215084","article-title":"Completion of a set of rules modulo a set of equations","volume":"15","author":"Jouannaud","year":"1986","journal-title":"SIAM J. on Computing"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0530","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1016\/0020-0190(82)90107-7","article-title":"On multiset orderings","volume":"15","author":"Jouannaud","year":"1982","journal-title":"Information Processing Letters"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0535","series-title":"Proceedings of the Second IFIP Workshop on Formal Description of Programming Concepts","first-page":"331","article-title":"Recursive decomposition ordering","author":"Jouannaud","year":"1982"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0540","series-title":"Proceedings of the Eighteenth EATCS Colloquium on Automata, Languages and Programming (Madrid, Spain)","first-page":"455","article-title":"Satisfiability of systems of ordinal notations with the subterm property is decidable","volume":"Vol. 510","author":"Jouannaud","year":"1991"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0545","series-title":"Two generalizations of the recursive path ordering","author":"Kamin","year":"1980"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50011-4_bb0550","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1016\/S0747-7171(87)80010-X","article-title":"Simplifying conditional term rewriting systems: Unification, termination and confluence","volume":"4","author":"Kaplan","year":"1987","journal-title":"J. Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50011-4_rf0545","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1016\/0304-3975(86)90005-8","article-title":"Rewriting with a nondeterministic choice operator","volume":"56","author":"Kaplan","year":"1988","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50011-4_bb0560","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1016\/S0747-7171(88)80019-1","article-title":"Only prime superpositions need be considered in the Knuth-Bendix procedure","volume":"6","author":"Kapur","year":"1988","journal-title":"Journal of Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0565","series-title":"Proceedings of the Ninth International Joint Conference on Artificial Intelligence","first-page":"1146","article-title":"An equational approach to theorem proving in first-order predicate calculus","author":"Kapur","year":"1985"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0570","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1016\/0304-3975(85)90023-4","article-title":"A finite Thue system with decidable word problem and without equivalent finite canonical system","volume":"35","author":"Kapur","year":"1985","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50011-4_bb0575","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1016\/0890-5401(90)90023-B","article-title":"On ground confluence of term rewriting systems","volume":"86","author":"Kapur","year":"1990","journal-title":"Information and Computation"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0580","series-title":"Proceedings of the Eighth International Conference on Rewriting Techniques and Applications (Barcelona, Spain)","first-page":"142","article-title":"A total, ground path ordering for proving termination of AC-rewrite systems","volume":"Vol. 1232","author":"Kapur","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0585","series-title":"A case study of the completion procedure: Proving ring commutativity problems","author":"Kapur","year":"1989"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50011-4_bb0590","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1006\/inco.1995.1075","article-title":"Transfinite reductions in orthogonal term rewriting systems","volume":"119","author":"Kennaway","year":"1995","journal-title":"Information and Computation"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50011-4_bb0595","first-page":"9","article-title":"Deduction with symbolic constraints","volume":"4","author":"Kirchner","year":"1990","journal-title":"RAIRO Theoretical Informatics and Applications"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0600","series-title":"2nd International Workshop on Conditional and Typed Rewriting Systems (Montreal, Canada)","first-page":"143","article-title":"Meta-rule synthesis from crossed rewrite systems","author":"Kirchner","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0605","article-title":"Combinatory Reduction Systems","author":"Klop","year":"1980"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0610","first-page":"1","article-title":"Term rewriting systems","volume":"Vol. 2","author":"Klop","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0615","series-title":"Computational Problems in Abstract Algebra","first-page":"263","article-title":"Simple word problems in universal algebras","author":"Knuth","year":"1970"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0620","series-title":"Knuth-Bendix constraint solving is NP-complete","author":"Korovin","year":"2000"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0625","series-title":"Proceedings of the Twelfth International Conference on Rewriting Techniques and Applications","article-title":"Verifying orientability of rewrite rules using the Knuth-Bendix order","author":"Korovin","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0630","series-title":"Proceedings of the Ninth International Conference on Automated Deduction (Argonne, Illinois)","first-page":"527","article-title":"On word problems in Horn theories","volume":"Vol. 310","author":"Kounalis","year":"1988"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0635","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1016\/0304-3975(85)90175-6","article-title":"On recursive path ordering","volume":"40","author":"Krishnamoorthy","year":"1985","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0640","first-page":"210","article-title":"Well-quasi-ordering, the tree theorem, and Vazsonyi's conjecture","volume":"95","author":"Kruskal","year":"1960","journal-title":"Transactions of the American Mathematical Society"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0645","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0020-0190(90)90221-I","article-title":"Modular term rewriting systems and the termination","volume":"34","author":"Kurihara","year":"1990","journal-title":"Information Processing Letters"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0650","series-title":"Proceedings of the Seventh International Conference on Automated Deduction (Napa, CA)","first-page":"128","article-title":"A progress report on new decision algorithms for finitely presented Abelian groups","volume":"Vol. 170","author":"Lankford","year":"1984"},{"key":"10.1016\/B978-044450813-3\/50011-4_rf0645","series-title":"Canonical inference, Memo ATP-32, Automatic Theorem Proving Project","author":"Lankford","year":"1975"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0660","series-title":"Some approaches to equality for computational logic: A survey and assessment, Memo ATP-36, Automatic Theorem Proving Project","author":"Lankford","year":"1977"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0665","series-title":"On proving term rewriting systems are Noetherian, Memo MTP-3","author":"Lankford","year":"1979"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0670","series-title":"The uniform word problem for J-algebras is decidable, Memo MTP-10","author":"Lankford","year":"1980"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0675","series-title":"Decision procedures for simple equational theories with commutative-associative axioms: Complete sets of commutative-associative reductions, Memo ATP-39","author":"Lankford","year":"1977"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0680","series-title":"Canonical Forms in Finitely Presented Algebras","author":"Le Chenadec","year":"1985"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0685","series-title":"Proceedings of the Seventh International Conference on Automated Deduction (Napa, CA)","first-page":"166","article-title":"Term rewriting systems and algebra","volume":"Vol. 516","author":"Lescanne","year":"1984"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0690","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/BF00302640","article-title":"On the recursive decomposition ordering with lexicographical status and other related orderings","volume":"6","author":"Lescanne","year":"1990","journal-title":"J. Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0695","series-title":"Proceedings of the Third Hawaii International Conference on System Science","first-page":"789","article-title":"On the termination of Markov algorithms","author":"Manna","year":"1970"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0700","series-title":"Proceedings of the Sixth International Conference on Rewriting Techniques and Applications (Kaiserslautern, Germany)","first-page":"2","article-title":"Modularity of completeness revisited","volume":"Vol.914","author":"Marchiori","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0705","series-title":"Proc. Algebraic and Logic Programming","first-page":"107","article-title":"Unravelings and ultra-properties","volume":"Vol.1139","author":"Marchiori","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0710","first-page":"37","article-title":"A geometrical approach to multiset orderings","volume":"67","author":"Martin","year":"1989","journal-title":"Information Processing Letters"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0715","series-title":"Proceedings of the Tenth International Conference on Automated Deduction (Kaiserslautern, West Germany)","first-page":"366","article-title":"Ordered completion","volume":"Vol.449","author":"Martin","year":"1990"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50011-4_bb0720","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1023\/A:1005843212881","article-title":"Solution of the Robbins problem","volume":"19","author":"McCune","year":"1997","journal-title":"J. Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0725","series-title":"Otter 1.0 Users' Guide","author":"McCune","year":"1989"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50011-4_bb0730","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1016\/0020-0190(83)90009-1","article-title":"About the rewriting systems produced by the Knuth-Bendix completion algorithm","volume":"16","author":"M\u00e9tivier","year":"1983","journal-title":"Information Processing Letters"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0735","series-title":"Proceedings, 7th ACM Symposium on Principles of Programming Languages","first-page":"154","article-title":"On proving inductive properties of abstract data types","author":"Musser","year":"1980"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0740","series-title":"Proceedings of the 3rd International Conference on rewriting techniques and applications","first-page":"311","article-title":"Algebraic semantics and complexity of term rewriting systems","volume":"Vol.355","author":"Naoi","year":"1989"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0745","series-title":"Proceedings of the Annual Conference of the European Association of Computer Science Logic (Brno, Czech Republic)","first-page":"385","article-title":"RPO constraint solving is in NP","author":"Narendran","year":"1998"},{"issue":"4","key":"10.1016\/B978-044450813-3\/50011-4_bb0750","doi-asserted-by":"crossref","first-page":"833","DOI":"10.1017\/S0305004100003844","article-title":"On well-quasi-ordering finite trees","volume":"59","author":"Nash-Williams","year":"1963","journal-title":"Proceedings of the Cambridge Philosophical Society"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50011-4_bb0755","doi-asserted-by":"crossref","first-page":"356","DOI":"10.1145\/322186.322198","article-title":"Fast decision procedures based on congruence closure","volume":"27","author":"Nelson","year":"1980","journal-title":"J. of the Association for Computing Machinery"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50011-4_bb0760","doi-asserted-by":"crossref","first-page":"223","DOI":"10.2307\/1968867","article-title":"On theories with a combinatorial definition of equivalence\u201d","volume":"43","author":"Newman","year":"1942","journal-title":"Annals of Mathematics"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50011-4_rf0755","doi-asserted-by":"crossref","DOI":"10.1016\/0020-0190(93)90226-Y","article-title":"Simple LPO constraint solving methods","volume":"47","author":"Nieuwenhuis","year":"1993","journal-title":"Information Processing Letters"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0770","first-page":"371","article-title":"Paramodulation-based theorem proving","volume":"Vol. I","author":"Nieuwenhuis","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0775","doi-asserted-by":"crossref","first-page":"742","DOI":"10.1145\/96559.96569","article-title":"Unification in primal algebras, their powers and their varieties","volume":"37","author":"Nipkow","year":"1990","journal-title":"J. of the Association for Computing Machinery"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0780","article-title":"Computing in systems described by equations","volume":"Vol.58","author":"O'Donnell","year":"1977"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0785","series-title":"Proceedings of the 4th International Symposium on Functional and Logic Programming","first-page":"179","article-title":"On quasi-reductive and quasi-simplifying deterministic conditional rewrite systems","volume":"Vol.1722","author":"Ohlebusch","year":"1999"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50011-4_bb0790","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1016\/0304-3975(87)90100-9","article-title":"The Church-Rosser property for ground term rewriting systems is decidable","volume":"49","author":"Oyamaguchi","year":"1987","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0795","article-title":"Confluence Methods and the Word Problem in Universal Algebra","author":"Pedersen","year":"1984","journal-title":"PhD thesis, Emory University"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0800","series-title":"Proceedings of the European Conference on Computer Algebra: Research Contributions (Linz, Austria)","first-page":"422","article-title":"Obtaining complete sets of reductions and equations without using special unification algorithms","volume":"Vol.204","author":"Pedersen","year":"1985"},{"issue":"4","key":"10.1016\/B978-044450813-3\/50011-4_bb0805","first-page":"575","article-title":"The word problem in absorbing varieties","volume":"11","author":"Pedersen","year":"1985","journal-title":"Houston Journal of Mathematics"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0810","series-title":"Computers in Algebra","first-page":"103","article-title":"Computer solution of word problems in universal algebra","volume":"Vol.111","author":"Pedersen","year":"1988"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0815","series-title":"Proceedings of the Third International Conference on Rewriting Techniques and Applications (Chapel Hill, NC)","first-page":"574","article-title":"Morphocompletion for one-relation monoids","volume":"Vol.355","author":"Pedersen","year":"1989"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0820","article-title":"Confluence methods and the word problem in universal algebra","author":"Pedersen","year":"1984","journal-title":"PhD thesis, Emory University"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0825","series-title":"Proceedings of the 10th International Conference on Automated Deduction","first-page":"381","article-title":"Complete sets of reductions with constraints","author":"Peterson","year":"1990"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50011-4_bb0830","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1145\/322248.322251","article-title":"Complete sets of reductions for some equational theories","volume":"28","author":"Peterson","year":"1981","journal-title":"J. of the Association for Computing Machinery"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0835","article-title":"A recursively defined ordering for proving termination of term rewriting systems","author":"Plaisted","year":"1978","journal-title":"technical report R-78-943, University of Illinois at Urbana-Champaign, Urbana, IL"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0840","series-title":"Proceedings of the Eighth International Conference on Automated Deduction","first-page":"79","article-title":"A simple non-termination test for the Knuth-Bendix method","volume":"Vol.230","author":"Plaisted","year":"1986"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0845","series-title":"Proceedings of the First International Workshop on Conditional Term Rewriting Systems (Orsay, France)","first-page":"212","article-title":"A logic for conditional term rewriting systems","volume":"Vol.308","author":"Plaisted","year":"1987"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50011-4_bb0850","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1016\/0020-0190(85)90063-8","article-title":"The undecidability of self embedding for term rewriting systems","volume":"20","author":"Plaisted","year":"1985","journal-title":"Information Processing Letters"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0855","first-page":"273","article-title":"Equational reasoning and term rewriting systems","volume":"Vol. 1","author":"Plaisted","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0860","series-title":"Proceedings of the First International Conference on Rewriting Techniques and Applications (Dijon, France)","first-page":"287","article-title":"Fairness in term rewriting systems","volume":"Vol.202","author":"Porat","year":"1985"},{"issue":"4","key":"10.1016\/B978-044450813-3\/50011-4_rf0855","doi-asserted-by":"crossref","first-page":"772","DOI":"10.1145\/322217.322229","article-title":"Operational and semantic equivalence between recursive programs","volume":"27","author":"Raoult","year":"1980","journal-title":"J. of the Association for Computing Machinery"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0870","series-title":"Logic Programming: Functions, Relations, and Equations","first-page":"3","article-title":"On the relationship between logic and functional languages","author":"Reddy","year":"1986"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50011-4_bb0875","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1016\/S0747-7171(10)80005-7","article-title":"On the computational complexity and geometry of the first-order theory of the reals. III. Quantifier elimination","volume":"13","author":"Renegar","year":"1992","journal-title":"J. Symbolic Computation"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50011-4_bb0880","doi-asserted-by":"crossref","first-page":"160","DOI":"10.1145\/321738.321750","article-title":"Tree-manipulating systems and Church-Rosser theorems","volume":"20","author":"Rosen","year":"1973","journal-title":"J. of the Association for Computing Machinery"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0885","series-title":"Proceedings of the International Conference on Rewriting Techniques and Applications","first-page":"133","article-title":"A fully syntactic AC-RPO","volume":"Vol.1631","author":"Rubio","year":"1999"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0890","series-title":"Proceedings of the Fifth International Conference on Rewriting Techniques and Applications (Montreal, Canada)","article-title":"A precedence-based total AC-compatible ordering","author":"Rubio","year":"1993"},{"issue":"1&2","key":"10.1016\/B978-044450813-3\/50011-4_bb0895","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/S0747-7171(87)80023-8","article-title":"Path of subterms ordering and recursive decomposition ordering revisited","volume":"3","author":"Rusinowitch","year":"1987","journal-title":"J. Symbolic Computation"},{"issue":"1\/2","key":"10.1016\/B978-044450813-3\/50011-4_bb0900","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1007\/BF02573590","article-title":"A Noetherian and confluent rewrite system for idempotent semigroups","volume":"25","author":"Siekmann","year":"1982","journal-title":"Semigroup Forum"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0905","series-title":"To Mock a Mockingbird","author":"Smullyan","year":"1985"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0910","series-title":"Proceedings of the Third International Conference on Rewriting Techniques and Applications (Chapel Hill, NC)","first-page":"419","article-title":"Efficient ground completion: An O(n log n) algorithm for generating reduced sets of ground rewrite rules equivalent to a set of ground equations e","volume":"Vol.355","author":"Snyder","year":"1989"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50011-4_bb0915","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1016\/0020-0190(94)90032-9","article-title":"Generating polynomial orderings","volume":"49","author":"Steinbach","year":"1994","journal-title":"Information Processing Letters"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0920","first-page":"37","article-title":"The theory of representations for Boolean algebra","volume":"40","author":"Stone","year":"1936","journal-title":"Transactions of the American Mathematical Society"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0925","series-title":"A Decision Method for Elementary Algebra and Geometry","author":"Tarski","year":"1951"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0930","series-title":"Formal Methods and Semantics","first-page":"133","article-title":"Automata on infinite objects","volume":"Vol. B","author":"Thomas","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0935","article-title":"Probleme \u00fcber veranderungen von zeichenreihen nach gegeben regeln","volume":"10\/34","author":"Thue","year":"1914","journal-title":"Skr. Vid. Kristianaia I. Mat. Naturv. Klasse"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0940","series-title":"Proceedings of the Third International Conference on Rewriting Techniques and Applications","first-page":"462","article-title":"Fair termination is decidable for ground systems","volume":"Vol.355","author":"Tison","year":"1989"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50011-4_bb0945","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1145\/7531.7534","article-title":"On the Church-Rosser property for the direct sum of term rewriting systems","volume":"34","author":"Toyama","year":"1987","journal-title":"J. of the Association for Computing Machinery"},{"issue":"6","key":"10.1016\/B978-044450813-3\/50011-4_bb0950","doi-asserted-by":"crossref","first-page":"1275","DOI":"10.1145\/227683.227689","article-title":"Termination for direct sums of left-linear complete term rewriting systems","volume":"42","author":"Toyama","year":"1995","journal-title":"J. of the Association for Computing Machinery"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0955","doi-asserted-by":"crossref","first-page":"259","DOI":"10.1016\/0304-3975(92)00023-K","article-title":"Confluence by decreasing diagrams","volume":"126","author":"van Oostrom","year":"1994","journal-title":"Theoretical Computer Science"},{"issue":"5","key":"10.1016\/B978-044450813-3\/50011-4_bb0960","doi-asserted-by":"crossref","first-page":"984","DOI":"10.1145\/210118.210130","article-title":"A theory of using history for equational systems with applications","volume":"42","author":"Verma","year":"1995","journal-title":"J. of the Association for Computing Machinery"},{"key":"10.1016\/B978-044450813-3\/50011-4_rf0955","doi-asserted-by":"crossref","DOI":"10.3233\/FUN-2001-46305","article-title":"Algorithms and reductions for rewriting systems","author":"Verma","year":"2001","journal-title":"Fundamenta Informaticae"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0970","doi-asserted-by":"crossref","first-page":"355","DOI":"10.1016\/0304-3975(94)00135-6","article-title":"Termination proofs via the lexicographic path ordering yields multiply recursive derivation lengths","volume":"139","author":"Weiermann","year":"1995","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0975","series-title":"Proceedings of the Colloquium on Algebra, Combinatorics and Logic in Computer Science","article-title":"A criterion for eliminating unnecessary reductions in the Knuth-Bendix algorithm","author":"Winkler","year":"1983"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0980","series-title":"Recursive Function Theory and Logic","author":"Yasuhara","year":"1971"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0985","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1006\/jsco.1994.1003","article-title":"Termination of term rewriting: Interpretation and type elimination","volume":"17","author":"Zantema","year":"1994","journal-title":"J. Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb0990","doi-asserted-by":"crossref","first-page":"89","DOI":"10.3233\/FI-1995-24124","article-title":"Termination of term rewriting by semantic labelling","volume":"24","author":"Zantema","year":"1995","journal-title":"Fundamenta Informaticae"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50011-4_bb0995","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1006\/jsco.1994.1011","article-title":"A new method for the Boolean ring based theorem proving","volume":"17","author":"Zhang","year":"1994","journal-title":"J. Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50011-4_bb1000","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/BF02090774","article-title":"Unnecessary inferences in associative-commutative completion procedures","volume":"23","author":"Zhang","year":"1990","journal-title":"Mathematical Systems Theory"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50011-4_bb1005","first-page":"9","article-title":"On a technique of evaluation of propositions in symbolic logic","volume":"34","author":"Zhegalkin","year":"1927","journal-title":"Matematicheskii Sbornik"}],"container-title":["Handbook of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B9780444508133500114?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B9780444508133500114?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,1,17]],"date-time":"2025-01-17T05:26:40Z","timestamp":1737091600000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/B9780444508133500114"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9780444508133"],"references-count":200,"URL":"https:\/\/doi.org\/10.1016\/b978-044450813-3\/50011-4","relation":{},"subject":[],"published":{"date-parts":[[2001]]}}}