CSI^ho
CSI^ho is an automatic confluence prover for higher-order rewrite systems, based on CSI.
CSI
CSI is an automatic confluence prover for first-order rewrite systems.
IsaFoR/CeTA
CeTA is a tool that certifies (non)confluence (or (non)termination or completion or complexity proofs) provided by automatic tools. It is built using IsaFoR, the Isabelle Formalization of Rewriting.