cl-banner

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

Nach oben scrollen