• Maude

  • Referenced in 615 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 290 articles [sw02904]
  • paramodulation, and it includes facilities for term rewriting, term orderings, Knuth-Bendix completion, weighting...
  • VAMPIRE

  • Referenced in 203 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 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...
  • 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 context-sensitive 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...
  • BABEL

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

  • Referenced in 70 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 type-checker is able...
  • 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...
  • 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...
  • CiME

  • Referenced in 37 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 context-sensitive rewriting; the CARIBOO tool (developed at INRIA Nancy ... Grand-Est) for termination of rewriting under strategies; and the MTT tool (http://www.lcc.uma.es/ duran/MTT...
  • CoLoR

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

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