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.