CSI is an automatic confluence prover for first-order rewrite systems.
An extension to higher-order pattern rewrite systems is described here.
