Confluence Competition

Confluence Competition


Confluence provides a general notion of determinism and has been conceived as one of the central properties of rewriting. Confluence had been investigated in several formalisms of rewriting such as first-order rewriting, lambda-calculi, higher-order rewriting, constrained rewriting and conditional rewriting. In recent years the focus in confluence research has shifted towards the development of automatable techniques for confluence proofs. The confluence competition aims to foster the development of techniques for proving/disproving confluence automatically by setting up a dedicated competition among confluence tools.


The competition will be run completely automatically on a dedicated host. For the competition a set of confluence problems is submitted to each participating tool. Each tool is supposed to answer whether the given term rewriting system is confluent or not (in a fixed time). Each tool must give evidence for its answer in a human understandable format. The tool which correctly answers the maximum number of problems wins. Several categories are considered depending on types of rewriting formalism and definitions of confluence properties. See the webpage of the latest competition for more details.


Tools are available by following the links in the individual competition pages. The versions that ran in the full run can be tested online at CoCoWeb.

Mailing List

Researchers interested in the confluence competition are invited to join the CoCo mailing list:
  coco [AT]
Please contact Nao Hirokawa for subscribing to this mailing list.

Steering Committee

The steering committee can be contacted via email:
  coco-sc [AT]
The steering committee is assisted by Nao Hirokawa (JAIST, Japan) for matters related to COPS.