Bachelor’s Thesis, Master’s Thesis, Practical Course

The goal of this project is to formalize a proof-producing congruence closure algorithm [1]. Congruence closure is an important operation in automated theorem proving that determines which terms are equal under substitutivity of equality and a given set of equalities. Examples problems are to prove f(f(a, b), b) = a from the fact f(a, b) = b or that f(f(f(a))) = a and f(f(f(f(f(a))))) = a together imply f(a) = a. What makes the algorithm in question special is that it not only decides whether two terms are equal but it can provide a proof that certifies equality on demand.

In the project, we will employ Isabelle/HOL to first formalise an abstract version of the algorithm to prove its correctness. Depending on the kind of project and whether time permits, the algorithm should also be refined using Imperative HOL in order to obtain an efficient executable version of the algorithm.


Prerequisites: Experience with Isabelle/HOL

Advisor: Lukas Stevens

Professor: Prof. Tobias Nipkow