### 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

- automate confluence criteria,
- certify confluence proofs, and
- 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

P22467#### Contact

aart middeldorp at uibk dot ac dot at#### 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.