Software

CSI

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

CSI^ho

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

CeTA

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

ConCon

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.

FORT

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.

KBCV

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

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

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

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

TCT

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.

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.