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.

Members

• Aart Middeldorp
• Harald Zankl
• Bertram Felgenhauer
• Julian Nagele

FWF project number

Contact

Publications

Reachability, Confluence, and Termination Analysis with State-Compatible Automata
Bertram Felgenhauer and René Thiemann
Information and Computation 253(3), pp. 467 – 483, 2017.

Confluence for Term Rewriting: Theory and Automation
Bertram Felgenhauer
PhD thesis, University of Innsbruck, 2015.

Layer Systems for Proving Confluence
Bertram Felgenhauer, Aart Middeldorp, Harald Zankl, and Vincent van Oostrom
ACM Transactions on Computational Logic 16(2:14), pp. 1 – 32, 2015.

Labelings for Decreasing Diagrams
Harald Zankl, Bertram Felgenhauer, and Aart Middeldorp
Journal of Automated Reasoning 54(2), pp. 101 – 133, 2015.

Challenges in Automation of Rewriting
Harald Zankl
Habilitation thesis, University of Innsbruck, 2014.

Type Introduction for Runtime Complexity Analysis
Martin Avanzini and Bertram Felgenhauer
Proceedings of the 14th International Workshop on Termination (WST 2014),   pp. 1 – 5, 2014.

Conditional Confluence (System Description)
Thomas Sternagel and Aart Middeldorp
Proceedings of the Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications (RTA-TLCA 2014), Lecture Notes in Computer Science 8560, pp. 456 – 465, 2014.

Certification of Confluence Proofs using CeTA
Julian Nagele and René Thiemann
Proceedings of the 3rd International Workshop on Confluence (IWC 2014),   pp. 19 – 23, 2014.

Reachability Analysis with State-Compatible Automata
Bertram Felgenhauer and René Thiemann
Proceedings of the 8th International Conference on Language and Automata Theory and Applications (LATA 2014), Lecture Notes in Computer Science 8370, pp. 347 – 359, 2014.

Decreasing Diagrams
Harald Zankl
Archive of Formal Proofs, 2013.

A Haskell Library for Term Rewriting
Bertram Felgenhauer, Martin Avanzini, and Christian Sternagel
Proceedings of the 1st International Workshop on Haskell and Rewriting Techniques (HART 2013),  2013.

Proof Orders for Decreasing Diagrams
Bertram Felgenhauer and Vincent van Oostrom
Proceedings of the 24th International Conference on Rewriting Techniques and Applications (RTA 2013), Leibniz International Proceedings in Informatics 21, pp. 174 – 189, 2013.

Commutation via Relative Termination
Nao Hirokawa and Aart Middeldorp
Proceedings of the 2nd International Workshop on Confluence (IWC 2013),   pp. 29 – 33, 2013.

Rule Labeling for Confluence of Left-Linear Term Rewrite Systems
Bertram Felgenhauer
Proceedings of the 2nd International Workshop on Confluence (IWC 2013),   pp. 23 – 27, 2013.

Confluence by Decreasing Diagrams – Formalized
Harald Zankl
Proceedings of the 24th International Conference on Rewriting Techniques and Applications (RTA 2013), Leibniz International Proceedings in Informatics 21, pp. 352 – 367, 2013.

Multi-Completion with Termination Tools
Sarah Winkler, Haruhiko Sato, Aart Middeldorp, and Masahito Kurihara
Journal of Automated Reasoning 50(3), pp. 317 – 354, 2013.

KBCV – Knuth-Bendix Completion Visualizer
Thomas Sternagel and Harald Zankl
Proceedings of the 6th International Joint Conference on Automated Reasoning (IJCAR 2012), Lecture Notes in Artificial Intelligence 7364, pp. 530 – 536, 2012.

CoCo 2012 Participant: CSI
Harald Zankl, Bertram Felgenhauer, and Aart Middeldorp
Proceedings of the 1st International Workshop on Confluence (IWC 2012),  2012.

Recording Completion for Finding and Certifying Proofs in Equational Logic
Thomas Sternagel, René Thiemann, Harald Zankl, and Christian Sternagel
Proceedings of the 1st International Workshop on Confluence (IWC 2012),   pp. 31 – 36, 2012.

IaCOP: Interface for the Administration of Cops
Christian Nemeth, Harald Zankl, and Nao Hirokawa
Proceedings of the 1st International Workshop on Confluence (IWC 2012),   pp. 21 – 24, 2012.

A Proof Order for Decreasing Diagrams
Bertram Felgenhauer
Proceedings of the 1st International Workshop on Confluence (IWC 2012),   pp. 7 – 13, 2012.

Deciding Confluence of Ground Term Rewrite Systems in Cubic Time
Bertram Felgenhauer
Proceedings of the 23rd International Conference on Rewriting Techniques and Applications (RTA 2012), Leibniz International Proceedings in Informatics 15, pp. 165 – 175, 2012.

Layer Systems for Proving Confluence
Bertram Felgenhauer, Harald Zankl, and Aart Middeldorp
Proceedings of the 30th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011), Leibniz International Proceedings in Informatics 13, pp. 288 – 299, 2011.

Decreasing Diagrams and Relative Termination
Nao Hirokawa and Aart Middeldorp
Journal of Automated Reasoning 47(4), pp. 481 – 501, 2011.

CSI – A Confluence Tool
Harald Zankl, Bertram Felgenhauer, and Aart Middeldorp
Proceedings of the 23rd International Conference on Automated Deduction (CADE 2011), Lecture Notes in Artificial Intelligence 6803, pp. 499 – 505, 2011.

Labelings for Decreasing Diagrams
Harald Zankl, Bertram Felgenhauer, and Aart Middeldorp
Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA 2011), Leibniz International Proceedings in Informatics 10, pp. 377 – 392, 2011.

Revisiting Matrix Interpretations for Polynomial Derivational Complexity of Term Rewriting
Friedrich Neurauter, Harald Zankl, and Aart Middeldorp
Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-17), Lecture Notes in Computer Science (Advanced Research in Computing and Software Science) 6397, pp. 550 – 564, 2010.

Decreasing Diagrams and Relative Termination
Nao Hirokawa and Aart Middeldorp
Proceedings of the 5th International Joint Conference on Automated Reasoning (IJCAR 2010), Lecture Notes in Artificial Intelligence 6173, pp. 487 – 501, 2010.