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 which 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 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.

The first step of the project is to prove the usefulness of the current unification hints framework in Isabelle. As part of this, a simple method to apply theorems to a goal statement modulo unification hints should be written.

The second step of the project is to extend the full higher-order unification algorithm to work with unification hints.

Finally, larger case studies and methods, such as a non-trivial reification tactic, should be implemented.

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

Advisor: Kevin Kappelmann

Supervisor: Prof. Tobias Nipkow