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.


Current Members

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

Former Members

FWF project number




Nach oben scrollen