Central to the implementation of a theorem prover is the concept of unification, the process of taking two logical terms A and B and finding a substitution θ such that θ(A) and θ(B) are equal. Conventional first-order terms (i.e. trees of symbols) have a straightforward structural algorithm from Robinson, but for the higher order case where terms may include λ-abstractions, the problem is undecidable in general. Miller identified a decidable subset of this higher-order case called pattern unification, which is widely used in theorem provers and proof assistants today.
Holbert is a browser-based graphical theorem prover implemented in Haskell whose terms are given in untyped λ-calculus. It is designed to be used as an educational tool. Currently, it uses pattern unification extensively to implement its unification engine, however this places strict requirements on the formatting of some rules to cooperate well with the unification engine.
This project would be focused on implementing some of the extensions to pattern unification to make this algorithm more flexible, starting with η-contraction of pattern arguments, and generalising potentially to the tricks talked about by András Kovács here and here.
Required Skills: Haskell Programming, Logic, λ-calculus