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 unique normal forms,
4. 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

• Julian Nagele
• Franziska Rapp
• Harald Zankl

FWF project number

Contact

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.