Confluence: Automation, Certification, Extensions

This project is concerned with confluence of term rewrite systems. In contrast to termination, automating confluence conditions is a research topic which has received little attention so far and we are not aware of any efforts towards certification. The aim of this project is to change this. More precisely, the aims are to

  1. automate confluence criteria,
  2. certify confluence proofs, and
  3. extend confluence research.

The first aim is to automate sufficient conditions for confluence that go beyond the techniques implemented in ACP, a confluence prover which was recently developed in Japan. This will stimulate research for new criteria and as a long-term effect we intend to establish an international competition for confluence tools (similar to the existing competition for termination provers).
Various bugs in termination provers have shown the need for independent certification of the tools’ output. The second aim of the project is to certify confluence proofs. To this end powerful sufficient criteria for confluence will be formalised and a format for representing proofs will be designed.
The third aim of the project is to extend confluence research. One extension is concerned with a variation of the Knuth-Bendix completion procedure to derive confluent systems in the absence of termination. Another extension is to lift sufficient criteria to higher-order rewrite systems. The third topic for extensions is concerned with extending known results for orthogonal rewrite systems to a larger class of confluent rewrite systems.

  • Aart Middeldorp
  • Harald Zankl
  • Bertram Felgenhauer
  • Julian Nagele
FWF project number



Nach oben scrollen