• Maude

• Referenced in 677 articles [sw06233]
• language and system supporting both equational and rewriting logic specification and programming for a wide ... equational specification and programming, Maude also supports rewriting logic computation...

• OTTER

• Referenced in 316 articles [sw02904]
• paramodulation, and it includes facilities for term rewriting, term orderings, Knuth-Bendix completion, weighting...

• VAMPIRE

• Referenced in 241 articles [sw02918]
• tautology deletion (optionally modulo commutativity), subsumption resolution, rewriting by ordered unit equalities, and a lightweight...

• Mace4

• Referenced in 211 articles [sw06905]
• decision procedure based on ground equational rewriting is applied. If satisfiability is detected...

• ELAN

• Referenced in 108 articles [sw02179]
• function evaluation principle based on rewriting. But rewriting is inherently non-deterministic since several rules ... This is in contrast to many existing rewriting-based languages where the term reduction strategy ... strategy operators and define them by rewrite rules. Evaluation of strategy application is itself based ... rewriting. So the simple and well-known paradigm of rewriting provides both the logical framework...

• AProVE

• Referenced in 153 articles [sw07831]
• systems for automated termination proofs of term rewrite systems (TRSs). It is the first tool...

• Stratego

• Referenced in 75 articles [sw01259]
• program transformation. The Stratego language provides rewrite rules for expressing basic transformations, programmable rewriting strategies ... syntax of the object language, and dynamic rewrite rules for expressing context-sensitive transformations, thus...

• REVE

• Referenced in 68 articles [sw28907]
• Computer experiments with the REVE term rewriting system generator. A term rewriting system generator called ... REVE builds confluent and uniformly terminating term rewriting systems from sets of equations. Particular emphasis...

• PYTHIA8

• Referenced in 108 articles [sw09347]
• Fortran, Pythia 8 represents a complete rewrite in C++. The current release is the first...

• Tyrolean

• Referenced in 89 articles [sw07830]
• automatically proving (and disproving) termination of term rewrite systems. It is the completely redesigned successor...

• RRL

• Referenced in 55 articles [sw28904]
• overview of Rewrite Rule Laboratory (RRL). RRL (Rewrite Rule Laboratory) was originally developed ... reasoning algorithms for equational logic based on rewrite techniques. It has now matured into...

• CLEAN

• Referenced in 58 articles [sw01346]
• functional language based on Term Graph Rewriting. It is specially designed to make the development ... Clean among which it’s Term Graph Rewriting semantics. Of particular importance for practical...

• Cactus

• Referenced in 79 articles [sw04422]
• release of Cactus (Version 4.0) a complete rewrite of earlier versions, which enables highly modular...

• BABEL

• Referenced in 71 articles [sw03018]
• lazy reduction semantics which embodies both rewriting and SLD resolution and supports computation with potentially...

• PROGRES

• Referenced in 70 articles [sw02905]
• type concept. It supports programming with graph rewriting systems. An integrated type-checker is able...

• K Prover

• Referenced in 42 articles [sw32257]
• original language or calculus syntax. K (rewrite) rules generalize conventional rewrite rules by making explicit ... handled like any other terms in a rewriting environment, that is, they can be matched...

• Timbuk

• Referenced in 47 articles [sw06351]
• achieving proofs of reachability over Term Rewriting Systems and for manipulating Tree Automata (bottom ... manipulation on Tree Automata, alphabets, terms, Term Rewriting Systems...

• CeTA

• Referenced in 46 articles [sw06584]
• automatic tools to prove termination of term rewrite systems, nowadays. Most of these tools ... first formalized the required theory of term rewriting including three major termination criteria: dependency pairs...

• MU-TERM

• Referenced in 34 articles [sw10015]
• Tool for Proving Termination of Context-Sensitive Rewriting. Restrictions of rewriting can eventually achieve termination ... pruning all infinite rewrite sequences issued from every term. Context-sensitive rewriting ... different ways, for proving termination of ordinary rewriting. Proofs of termination of CSR are also...

• CoLoR

• Referenced in 38 articles [sw09806]
• CoLoR: a Coq library on well-founded rewrite relations and its application to the automated ... Turing-complete formalism of term rewriting. Over the years, many methods and tools have been ... results of the theory of well-founded (rewrite) relations in the proof assistant...