Bachelor’s Thesis, Practical Course, Master’s thesis
The goal of this project is to implement a decision procedure for multi-level syllogistic with singleton (MLSS). This is a quantifier-free fragment of set theory with the usual set operation such as union and intersection as well as the singleton operator \(\{\cdot\}\), where \(\{e\}\) constructs the singleton set only containing \(e\). An abstract specification of this decision procedure is already formalised in the AFP entry MLSS Decision Procedure Starting from this point, one can either refine the abstract specification into an executable specification from which code can be extracted, or one implements the procedure directly in Isabelle/ML to evaluate its usefulness in practice.
In the project, we will either employ Isabelle/HOL to refine an existing formal specification or use Isabelle/ML to implement a tactic that applies the decision procedure.
Prerequisites: Experience with Isabelle/HOL or experience with functional programming (ideally in Isabelle/ML)
Advisor: Lukas Stevens
Professor: Prof. Tobias Nipkow