cl-banner

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

P22467

  Contact

aart.middeldorp@uibk.ac.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.
Nach oben scrollen