
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, KnuthBendix 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 nondeterministic since several rules ... This is in contrast to many existing rewritingbased 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 wellknown 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 contextsensitive 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 typechecker 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...

MUTERM
 Referenced in 34 articles
[sw10015]
 Tool for Proving Termination of ContextSensitive Rewriting. Restrictions of rewriting can eventually achieve termination ... pruning all infinite rewrite sequences issued from every term. Contextsensitive 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 wellfounded rewrite relations and its application to the automated ... Turingcomplete formalism of term rewriting. Over the years, many methods and tools have been ... results of the theory of wellfounded (rewrite) relations in the proof assistant...