CSI is an automatic confluence prover for first-order rewrite systems. It is based on the Tyrolean Termination Tool 2.
CeTA is a tool that certifies automatically generated proofs provided by a termination (or confluence or complexity or completion) tool.
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.
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.