Bachelor’s Thesis, Master’s Thesis
The goal of this project is to formalise the Nelson-Oppen combination of theories [1]. By employing a congruence closure algorithm, one can combine two or more disjoint theories into one unified theory, e.g. one can combine the theory of arrays and the theory of reals into one theory. This makes it a key building block of Satisfiability Modulo Theories (SMT). More specifically, the goal is to use a proof-producing congruence closure algorithm in order to combine several proof-producing decision procedures of disjoint theories into one proof-producing decision procedure.
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] Simplification by Cooperating Decision Procedures [2] Combining Decision Procedures (Survey Paper) [3] Proof-Producing Congruence Closure
Prerequisites: Experience with Isabelle/HOL
Advisor: Lukas Stevens
Professor: Prof. Tobias Nipkow