
Maude
 Referenced in 613 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 286 articles
[sw02904]
 paramodulation, and it includes facilities for term rewriting, term orderings, KnuthBendix completion, weighting...

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

ELAN
 Referenced in 100 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...

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

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

Stratego
 Referenced in 72 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 67 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 97 articles
[sw09347]
 Fortran, Pythia 8 represents a complete rewrite in C++. The current release is the first...

Tyrolean
 Referenced in 88 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 56 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...

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

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

PROGRES
 Referenced in 68 articles
[sw02905]
 type concept. It supports programming with graph rewriting systems. An integrated typechecker is able...

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...

Timbuk
 Referenced in 43 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...

CoLoR
 Referenced in 36 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...

CiME
 Referenced in 36 articles
[sw09970]
 CiME is a rewriting toolbox. Distributed since 1996 as open source, at URL http://cime.lri.fr ... www.dsic.upv.es/ slucas/csr/termination/muterm/ ) for termination of contextsensitive rewriting; the CARIBOO tool (developed at INRIA Nancy ... GrandEst) for termination of rewriting under strategies; and the MTT tool (http://www.lcc.uma.es/ duran/MTT...

AIDA
 Referenced in 57 articles
[sw11535]
 invariants: computation of generating sets of invariants, rewritings, syzygies, and their differential analogues. The package...