From Confluence to Unique Normal Forms: Certification and Complexity


This project is about confluence and the related unique normal form property of rewrite systems. In the preceding years many powerful confluence methods have been developed and implemented in confluence tools that participate in the recently established confluence competition. Important first steps towards certification have been made, but much remains to be done. The aim of this successor project is to fill two important gaps concerning certification, investigate methods for the unique normal form property, study various complexity issues related to confluence and unique normal forms, and further develop the confluence tool CSI and the certification tool CeTA for confluence. More precisely, the aims are to

  1. formalize the layer framework that captures important divide and conquer results for confluence like layer-preservation and modularity into a single abstract framework,
  2. develop a formalized proof for the confluence of development closed left-linear (higher-order pattern) rewrite system based on proof terms and residual theory,
  3. investigate conditional linearization and related techniques like Chew’s theorem to obtain automatable techniques for
  4. unique normal forms, study (tractable) decidable classes for confluence and unique normal forms as well as ways to lower the complexity of the various search problems that underlie concrete confluence methods,
  5. use the insights gained in the previous items to increase the confluence proving power and efficiency of the automatic confluence tool CSI and the automatic certification tool CeTA with regard to confluence.


Members

Current Members

  • Bertram Felgenhauer
  • Aart Middeldorp
  • Christina Kohl
  • Fabian Mitterwallner

Former Members

 
FWF project number

P27528

  Contact

aart.middeldorp@uibk.ac.at

Publications
  • Abstract Completion, Formalized
    Nao Hirokawa, Aart Middeldorp, Christian Sternagel, Sarah Winkler
    Logical Methods in Computer Science,  15(3), pp. 19:1 – 19:42, 2019.
  • Composing Proof Terms
    Christina Kohl and Aart Middeldorp
    27th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence 11716, pp. 337 – 353, 2019.
  • Residuals Revisited
    Christina Kohl and Aart Middeldorp
    Joint Proceedings of the 10th Workshop on Higher-Order Rewriting (HOR 2019) and the 7th International Workshop on Confluence (IWC 2019),   pp. 43 – 47, 2019.
  • CoCo 2019 Participant: CSI 1.2.3
    Bertram Felgenhauer, Aart Middeldorp, and Fabian Mitterwallner
    Joint Proceedings of the 10th Workshop on Higher-Order Rewriting (HOR 2019) and the 7th International Workshop on Confluence (IWC 2019),   pp. 54, 2019.
  • Confluence Competition 2019
    Aart Middeldorp, Julian Nagele, and Kiraku Shintani
    Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019, part III), Lecture Notes in Computer Science 11429, pp. 25 – 40, 2019.
  • Deciding Confluence and Normal Form Properties of Ground Term Rewrite Systems Efficiently
    Bertram Felgenhauer
    Logical Methods in Computer Science 14(4:7), pp. 1 – 35, 2018.
  • Layer Systems for Confluence — Formalized
    Bertram Felgenhauer and Franziska Rapp
    Proceedings of the 15th International Colloquium on Theoretical Aspects of Computing (ICTAC 2018), Lecture Notes in Computer Science 11187, pp. 173 – 190, 2018.
  • Confluence Competition 2018
    Takahito Aoto, Makoto Hamana, Nao Hirokawa, Aart Middeldorp, Julian Nagele, Naoki Nishida, Kiraku Shintani, and Harald Zankl
    Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), Leibniz International Proceedings in Informatics 108, pp. 32:1 – 32:5, 2018.
  • ProTeM: A Proof Term Manipulator (System Description)
    Christina Kohl and Aart Middeldorp
    Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), Leibniz International Proceedings in Informatics 108, pp. 31:1 – 31:8, 2018.
  • CoCo 2018 Participant: CSI 1.2.1
    Bertram Felgenhauer, Aart Middeldorp, Fabian Mitterwallner, and Julian Nagele
    Proceedings of the 7th International Workshop on Confluence (IWC 2018),   pp. 76, 2018.
  • CoCo 2018 Participant: CSI^ho 0.3.2
    Julian Nagele
    Proceedings of the 7th International Workshop on Confluence (IWC 2018),   pp. 68, 2018.
  • CoCo 2018 Participant: CeTA 2.33
    Bertram Felgenhauer, Franziska Rapp, Christian Sternagel and Sarah Winkler
    Proceedings of the 7th International Workshop on Confluence (IWC 2018),   pp. 63, 2018.
  • Cops and CoCoWeb: Infrastructure for Confluence Tools
    Nao Hirokawa, Julian Nagele, and Aart Middeldorp
    Proceedings of the 9th International Joint Conference on Automated Reasoning (IJCAR 2018), Lecture Notes in Artificial Intelligence 10900, pp. 346 – 353, 2018.
  • Mechanizing Confluence: Automated and Certified Analysis of First- and Higher-Order Rewrite Systems
    Julian Nagele
    PhD thesis, University of Innsbruck, 2017.
  • Beyond DRAT: Challenges in Certifying UNSAT
    Bertram Felgenhauer
    Proceedings of the 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements (ARCADE 2017), EPiC Series in Computing 51, pp. 46 – 50, 2017.
  • Constructing Cycles in the Simplex Method for DPLL(T)
    Bertram Felgenhauer and Aart Middeldorp
    Proceedings of the 14th International Colloquium on Theoretical Aspects of Computing (ICTAC 2017), Lecture Notes in Computer Science 10580, pp. 213 – 228, 2017.
  • CoCo 2017 Participant: FORT 1.0
    Franziska Rapp and Aart Middeldorp
    Proceedings of the 6th International Workshop on Confluence (IWC 2017),   pp. 78, 2017.
  • CoCo 2017 Participant: CSI^ho 0.3
    Julian Nagele
    Proceedings of the 6th International Workshop on Confluence (IWC 2017),   pp. 77, 2017.
  • CoCo 2017 Participant: CSI 1.1
    Bertram Felgenhauer, Aart Middeldorp, and Julian Nagele
    Proceedings of the 6th International Workshop on Confluence (IWC 2017),   pp. 76, 2017.
  • CoCoWeb — A Convenient Web Interface for Confluence Tools
    Julian Nagele and Aart Middeldorp
    Proceedings of the 6th International Workshop on Confluence (IWC 2017),   pp. 39 – 44, 2017.
  • Formalized Ground Completion
    Aart Middeldorp and Christian Sternagel
    Proceedings of the 6th International Workshop on Confluence (IWC 2017),   pp. 51 – 55, 2017.
  • Infinite Runs in Abstract Completion
    Nao Hirokawa, Aart Middeldorp, Sarah Winkler, and Christian Sternagel
    Proceedings of the 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017), Leibniz International Proceedings in Informatics 84, pp. 19:1 – 19:16, 2017.
  • Aspects of Layer Systems in IsaFoR
    Bertram Felgenhauer, Franziska Rapp
    Proceedings of the 6th International Workshop on Confluence (IWC 2017),   pp. 63 – 67, 2017.
  • CSI: New Evidence – A Progress Report
    Julian Nagele, Bertram Felgenhauer, and Aart Middeldorp
    Proceedings of the 26th International Conference on Automated Deduction (CADE-26), Lecture Notes in Artificial Intelligence 10395, pp. 385 – 397, 2017.
  • Certifying Confluence Proofs via Relative Termination and Rule Labeling
    Julian Nagele, Bertram Felgenhauer, and Harald Zankl
    Logical Methods in Computer Science,  13(2:4), pp. 1 – 27, 2017.
  • Reachability, Confluence, and Termination Analysis with State-Compatible Automata
    Bertram Felgenhauer and René Thiemann
    Information and Computation 253(3), pp. 467 – 483, 2017.
  • A Short Mechanized Proof of the Church-Rosser Theorem by the Z-property for the λβ-calculus in Nominal Isabelle
    Julian Nagele, Vincent van Oostrom, and Christian Sternagel
    Proceedings of the 5th International Workshop on Confluence (IWC 2016),   pp. 55 – 59, 2016.
  • Efficiently Deciding Uniqueness of Normal Forms and Unique Normalization for Ground TRSs
    Bertram Felgenhauer
    Proceedings of the 5th International Workshop on Confluence (IWC 2016),   pp. 16 – 20, 2016.
  • CoCo 2016 Participant: FORT 1.0
    Franziska Rapp and Aart Middeldorp
    Proceedings of the 5th International Workshop on Confluence (IWC 2016),   pp. 86, 2016.
  • Confluence Properties on Open Terms in the First-Order Theory of Rewriting
    Franziska Rapp and Aart Middeldorp
    Proceedings of the 5th International Workshop on Confluence (IWC 2016),   pp. 26 – 30, 2016.
  • CoCo 2016 Participant: CSI^ho 0.2
    Julian Nagele
    Proceedings of the 5th International Workshop on Confluence (IWC 2016),   pp. 85, 2016.
  • CoCo 2016 Participant: CSI 0.6
    Bertram Felgenhauer, Aart Middeldorp, and Julian Nagele
    Proceedings of the 5th International Workshop on Confluence (IWC 2016),   pp. 84, 2016.
  • CoCo 2016 Participant: CeTA 2.28
    Julian Nagele, Christian Sternagel, and Thomas Sternagel
    Proceedings of the 5th International Workshop on Confluence (IWC 2016),   pp. 78, 2016.
  • Certification of Classical Confluence Results for Left-Linear Term Rewrite Systems
    Julian Nagele and Aart Middeldorp
    Proceedings of the 7th International Conference on Interactive Theorem Proving (ITP 2016), Lecture Notes in Computer Science 9807, pp. 290 – 306, 2016.
  • Automating the First-Order Theory of Left-Linear Right-Ground Term Rewrite Systems
    Franziska Rapp and Aart Middeldorp
    Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016), Leibniz International Proceedings in Informatics 52, pp. 36:1 – 36:12, 2016.
  • The Z Property
    Bertram Felgenhauer, Julian Nagele, Vincent van Oostrom, and Christian Sternagel
    The Archive of Formal Proofs,  2016.
  • CoCo 2015 Participant: CSIˆho 0.1
    Julian Nagele
    Proceedings of the 4th International Workshop on Confluence (IWC 2015),   pp. 47, 2015.
  • CoCo 2015 Participant: CSI 0.5.1
    Bertram Felgenhauer, Aart Middeldorp, Julian Nagele, and Harald Zankl
    Proceedings of the 4th International Workshop on Confluence (IWC 2015),   pp. 46, 2015.
  • CoCo Participant: CeTA 2.21
    Julian Nagele, Christian Sternagel, Thomas Sternagel, René Thiemann, Sarah Winkler, and Harald Zankl
    Proceedings of the 4th International Workshop on Confluence (IWC 2015),   pp. 41, 2015.
  • Labeling Multi-Steps for Confluence of Left-Linear Term Rewrite Systems
    Bertram Felgenhauer
    Proceedings of the 4th International Workshop on Confluence (IWC 2015),   pp. 33 – 37, 2015.
  • Point-Step-Decreasing Diagrams
    Bertram Felgenhauer
    Proceedings of the 4th International Workshop on Confluence (IWC 2015),   pp. 8 – 12, 2015.
  • Point-Decreasing Diagrams Revisited
    Bertram Felgenhauer
    Proceedings of the 4th International Workshop on Confluence (IWC 2015),   pp. 3 – 7, 2015.
  • Confluence Competition 2015
    Takahito Aoto, Nao Hirokawa, Julian Nagele, Naoki Nishida, and Harald Zankl
    Proceedings of the 25th International Conference on Automated Deduction (CADE-25), Lecture Notes in Artificial Intelligence 9195, pp. 101 – 104, 2015.
  • Certified Rule Labeling
    Julian Nagele and Harald Zankl
    Proceedings of the 26th International Conference on Rewriting Techniques and Applications (RTA 2015), Leibniz International Proceedings in Informatics 36, pp. 269 – 284, 2015.
  • Improving Automatic Confluence Analysis of Rewrite Systems by Redundant Rules
    Julian Nagele, Bertram Felgenhauer, and Aart Middeldorp
    Proceedings of the 26th International Conference on Rewriting Techniques and Applications (RTA 2015), Leibniz International Proceedings in Informatics 36, pp. 257 – 268, 2015.
Nach oben scrollen