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
Former Members

FWF project number

P27528

Contact

aart middeldorp at uibk dot ac dot at

Publications

Constructing Cycles in the Simplex Method for DPLL(T)
Bertram Felgenhauer, 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.

CoCoWeb — A Convenient Web Interface for Confluence Tools
Julian Nagele and Aart Middeldorp
Proceedings of the 6th International Workshop on Confluence,   pp. 39 – 44, 2017.

Formalized Ground Completion
Aart Middeldorp, Christian Sternagel
Proceedings of the 6th International Workshop on Confluence,   pp. 51 – 55, 2017.

Infinite Runs in Abstract Completion
Nao Hirokawa, Aart Middeldorp, Sarah Winkler, Christian Sternagel
2nd International Conference on Formal Structures for Computation and Deduction, Leibniz International Proceedings in Informatics 84, pp. 19:1-19:16, 2017.

Aspects of Layer Systems in IsaFoR
Bertram Felgenhauer, Franziska Rapp
6th International Workshop on Confluence (IWC 2017),   pp. 63 – 67, 2017.

CSI: New Evidence – A Progress Report
Julian Nagele, Bertram Felgenhauer, Aart Middeldorp
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, 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, 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.

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.