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

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

ELAN
 Referenced in 101 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 185 articles
[sw06905]
 decision procedure based on ground equational rewriting is applied. If satisfiability is detected...

AProVE
 Referenced in 141 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 99 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 57 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 72 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 68 articles
[sw02905]
 type concept. It supports programming with graph rewriting systems. An integrated typechecker is able...

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

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

CiME
 Referenced in 38 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...

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

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