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 latest competition for more details.

Steering Committee

Advisory Board


coco-sc [AT]



Former Members