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

- formalize the layer framework that captures important divide and conquer results for confluence like layer-preservation and modularity into a single abstract framework,
- develop a formalized proof for the confluence of development closed left-linear (higher-order pattern) rewrite system based on proof terms and residual theory,
- investigate conditional linearization and related techniques like Chew’s theorem to obtain automatable techniques for 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,
- 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

##### Former Members

- Julian Nagele
- Franziska Rapp
- Harald Zankl

#### FWF project number

P27528#### Contact

aart middeldorp at uibk dot ac dot at#### Publications

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

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, 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.