Bachelor’s Thesis or Practical Course

Unification algorithms can be used to prove the equality of two terms s=?=t while possibly instantiating variables. Unification hints are a controlled mechanism to extend such unification algorithms with new inference rules: if the unification algorithm fails, the set of collected unification hints is matched against the given terms to find an appropriate alternative.

This mechanism is particularly useful for interactive theorem provers such as Isabelle, where users can provide such hints to guide the unifier when facing seemingly trivial equalities that might not hold by pure unification but by using special domain knowledge. Beyond extending the strength of the unifier, unification hints can be used to build other mechanisms, such as type classes and reification tactics.

The goal of this project is to extend the existing framework of unification hints in Isabelle. Currently, the first-order and higher-order pattern unifier are able to work with unification hints. On top, the usefulness of unification hints should be proven by means of new and larger case studies, such as a non-trivial reification tactics, and improvements of existing formalisation using unification hints.

Prerequisites: good functional programming experience as well as basic experience with Isabelle.

Advisor: Kevin Kappelmann

Supervisor: Prof. Tobias Nipkow