CeTA

CeTA is a tool that certifies (non)termination or (non)confluence or completion or complexity proofs provided by some automated (termination/complexity/...) tool.

Version: 2.36

ConCon

ConCon is a fully automatic confluence checker for oriented first-order conditional term rewrite systems (CTRSs).

Version: 1.9.1.0

CSI

CSI is an automatic confluence prover for first-order rewrite systems.

Version: 1.2.2

CSI^ho

CSI^ho is an automatic confluence prover for higher-order rewrite systems, specifically pattern rewrite systems as introduced by Nipkow. It is based on CSI, a confluence prover for first-order term rewrite systems.

Version: 0.3.2

FORT

FORT is a decision and synthesis tool for the first-order theory of rewriting with respect to left-linear right-ground term rewrite systems.

Version: 2.0.1

MiniSmt

MiniSmt is an SMT-solver for quantifier-free non-linear arithmetic. In contrast to most competitor tools it can find models over irrational domains.

Version: 0.65

mkbTT

mkbTT is a tool for Knuth-Bendix completion: given a set of input equalities, it tries to generate a confluent and terminating rewrite system that can be used to decide the equational theory.

Version: 2.2

TCT - HoCA

The Tyrolean Complexity Tool (TCT for short) is a tool for automatically proving polynomial upper bounds on the derivational complexity and runtime complexity of term rewriting systems. TCT is open source and licensed under the GNU Lesser General Public License.

Version: 3.2

TCT - TRS

The Tyrolean Complexity Tool (TCT for short) is a tool for automatically proving polynomial upper bounds on the derivational complexity and runtime complexity of term rewriting systems. TCT is open source and licensed under the GNU Lesser General Public License.

Version: termcomp2018

TTT2

The Tyrolean Termination Tool 2 (TTT2) is a tool for automatically proving (and disproving) termination of rewrite systems. It is the completely redesigned successor of TTT.

Version: 1.19