• OTTER

  • Referenced in 204 articles [sw02904]
  • paramodulation, and it includes facilities for term rewriting, term orderings, Knuth-Bendix completion, weighting...
  • AProVE

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

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

  • Referenced in 59 articles [sw03160]
  • well-known library in the term rewriting community. In this paper, we discuss the current...
  • Timbuk

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

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

  • Referenced in 38 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...
  • MU-TERM

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

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

  • Referenced in 19 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...
  • TPA

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

  • Referenced in 9 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...
  • Jambox

  • Referenced in 11 articles [sw10066]
  • automated termination prover for string and term rewriting systems...
  • Boolector

  • Referenced in 9 articles [sw00085]
  • vectors and arrays. It uses term rewriting, bit-blasting to handle bit-vectors, and lemmas...
  • TXL

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

  • Referenced in 5 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...
  • CSI

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

  • Referenced in 6 articles [sw10104]
  • SbReve2: A term rewriting laboratory with (AC)-unfailing completion...
  • MicroRogue

  • Referenced in 4 articles [sw13590]
  • From Rogue to MicroRogue. The rewriting calculus has been proposed as a foundational system combining ... central ideas of $lambda$-calculus and term rewriting. The rewriting is explicit, in the sense ... terms to transform them. This paper begins with an imperative version of the rewriting calculus ... more foundational system called MicroRogue. MicroRogue rewrites terms using a global set of first-order...
  • VAMPIRE

  • Referenced in 151 articles [sw02918]
  • tautology deletion (optionally modulo commutativity), subsumption resolution, rewriting by ordered unit equalities, and a lightweight ... implement all major operations on sets of terms and clauses. Run-time algorithm specialisation...