Confluence Competition

Confluence Competition

Overview

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.

Procedure

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

The pointers to known confluence tools can be checked in the Entrants section of the latest competition. Confluence tools that participated in past competitions are available online at CoCoWeb. You might also be interested in the list of Tools on Rewriting maintained by Nao Hirokawa.

Mailing List

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

Steering Committee


The steering committee can be contacted via email:
  coco-sc [AT] informatik.uibk.ac.at