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) = a 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.
[1] https://link.springer.com/chapter/10.1007/978-3-540-32033-3_33
Prerequisites: Experience with Isabelle/HOL
Advisor: Lukas Stevens
Professor: Prof. Tobias Nipkow