Bertram Felgenhauer

From Confluence to Unique Normal Forms: Certification and Complexity

I am working on the Confluence and Unique Normal Forms project. This involved both extending our confluence prover, CSI, and formalizing results in IsaFoR for integration in the CeTA certifier.

Further information

Automating Confluence

This project has been completed.

As part of the Confluence Project, I am investigated and implemented criteria for proving confluence of term rewrite systems.

Further information