Software

CSI is an automatic confluence prover for first-order rewrite systems. It is based on the Tyrolean Termination Tool 2.

CSI^ho is an automatic confluence prover for higher-order rewrite systems, based on CSI.

CeTA is a tool that certifies automatically generated proofs provided by a termination (or confluence or complexity or completion) tool.

The conditional confluence tool, ConCon for short, is a fully automatic confluence checker for first-order conditional term rewrite systems. The tool implements various confluence criteria that have been proposed in the literature.

The first-order rewriting tool, FORT for short, is a decision and synthesis tool for the first-order theory of
of rewriting for finite left-linear right-ground rewrite systems.

The Knuth-Bendix Completion Visualizer (KBCV) is a tool that allows the user to interactively perform the Knuth-Bendix completion procedure. Furthermore the tool has been extended with recording completion which can be used to generate equational logic proof trees automatically. The completion proof and the generated proof trees are available in a certifiable xml format.

MKBtt is a completion tool for rewrite systems, which uses a termination tool to orient equations together with a special data structure to sequentialize the parallel execution of the processes that derive from choices in the orientation of equations.

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

ProTeM is a tool that offers support for manipulating proof terms that represent multisteps in left-linear rewrite systems.

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.

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.