Bertram Felgenhauer

FORTissimo: Automating the First-Order Theory of Rewriting

In the FORTissimo project, I have formalized constructions involving ground tree transducers (GTTs) and regular relations (RRn relations) in Isabelle/HOL.

From Confluence to Unique Normal Forms: Certification and Complexity

This project is almost complete.

I have worked 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.

Automating Confluence

This project has been completed.

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