
OTTER
 Referenced in 314 articles
[sw02904]
 paramodulation, and it includes facilities for term rewriting, term orderings, KnuthBendix completion, weighting...

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

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

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

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

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

ELAN
 Referenced in 108 articles
[sw02179]
 function evaluation principle based on rewriting. But rewriting is inherently nondeterministic since several rules ... applied at different positions in a same term, and in ELAN, a computation may have ... contrast to many existing rewritingbased languages where the term reduction strategy is hardwired ... strategy operators and define them by rewrite rules. Evaluation of strategy application is itself based...

ATERM
 Referenced in 43 articles
[sw03160]
 wellknown library in the term rewriting community. In this paper, we discuss the current...

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

Boolector
 Referenced in 28 articles
[sw00085]
 vectors and arrays. It uses term rewriting, bitblasting to handle bitvectors, and lemmas...

MUTERM
 Referenced in 34 articles
[sw10015]
 term: A Tool for Proving Termination of ContextSensitive Rewriting. Restrictions of rewriting can eventually ... rewrite sequences issued from every term. Contextsensitive rewriting (CSR) is an example of such ... permanently forbidden. This paper describes muterm, a tool which can be used to automatically ... first termination tool which generates term orderings based on such polynomial interpretations. These orderings...

K Prover
 Referenced in 41 articles
[sw32257]
 generalize conventional rewrite rules by making explicit which parts of the term they read, write ... handled like any other terms in a rewriting environment, that is, they can be matched ... place to another in the original term, modified, or even deleted, K is particularly suitable...

CSI
 Referenced in 22 articles
[sw09767]
 describes a new confluence tool for term rewrite systems. Due to its modular design...

TXL
 Referenced in 17 articles
[sw11319]
 programming at the higher level and term rewriting at the lower level, TXL provides...

Jambox
 Referenced in 14 articles
[sw10066]
 automated termination prover for string and term rewriting systems...

TPA
 Referenced in 13 articles
[sw10114]
 tool for proving termination of term rewrite systems (TRSs) in a fully automated fashion...

Autowrite
 Referenced in 8 articles
[sw01282]
 tool for checking properties of term rewriting systems Huet and Lévy have shown that ... class of orthogonal term rewriting systems (TRSs) every term not in normal form contains ... redex contracted in every normalizing rewrite sequence) and that repeated contraction of needed redexes results...

VMTL
 Referenced in 8 articles
[sw10065]
 automated analysis of termination of term rewriting systems (TRSs) has drawn a lot of attention ... analyzing the termination behaviour of conditional term rewriting systems (CTRSs). Using one of the latest...

HarmonicSums
 Referenced in 48 articles
[sw10035]
 nested sums and iterated integrals in terms of basis representations. Moreover, the package allows ... algorithm which rewrites certain types of nested sums into expressions in terms of cyclotomic...