• AProVE

  • Referenced in 143 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 ... basic manipulation on Tree Automata, alphabets, terms, Term Rewriting Systems...
  • CeTA

  • Referenced in 40 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...
  • OTTER

  • Referenced in 312 articles [sw02904]
  • current automated deduction system Otter is designed to prove theorems stated in first-order logic ... paramodulation, and it includes facilities for term rewriting, term orderings, Knuth-Bendix completion, weighting ... calculator and has an embedded equational programming system. Otter is a fourth-generation Argonne National...
  • CSI

  • Referenced in 21 articles [sw09767]
  • describes a new confluence tool for term rewrite systems. Due to its modular design...
  • 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...
  • Saigawa

  • Referenced in 9 articles [sw10102]
  • automatic confluence tool for first-order term rewrite systems. The latest version is based...
  • A3PAT

  • Referenced in 8 articles [sw21587]
  • based programming or specifications often use rewriting systems for which termination, among other properties ... with full automation, termination proofs for term rewriting systems. It consists of two developments...
  • CoLL

  • Referenced in 5 articles [sw13633]
  • confluence tool for left-linear term rewrite systems. We present a confluence tool for left ... linear term rewrite systems. The tool proves confluence by using Hindley’s commutation theorem together...
  • IsaFoR

  • Referenced in 5 articles [sw10106]
  • Isabelle/HOL by encoding them as term rewrite systems and invoking an external termination prover ... termination of the corresponding term rewrite system. We automate this reduction via suitable tactics which...
  • VAMPIRE

  • Referenced in 220 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 ... ordering constraints. Although the kernel of the system works only with clausal normal forms...
  • KITTeL

  • Referenced in 7 articles [sw17045]
  • compiler intermediate language are translated into term rewrite systems (TRSs), and the termination proof itself...
  • Conditional Confluence

  • Referenced in 6 articles [sw13315]
  • Conditional confluence (system description). This paper describes the Conditional Confluence tool, a fully automatic ... confluence checker for first-order conditional term rewrite systems. The tool implements various confluence criteria...
  • ConCon

  • Referenced in 2 articles [sw21589]
  • Reliable Confluence Checker for Conditional Term Rewrite Systems. ConCon is a fully automatic confluence checker ... oriented first-order conditional term rewrite systems (CTRSs). It is written in Scala and available...