(Nominal) Unification by Recursive Descent with Triangular Substitutions

Abstract

Using HOL4, we mechanise termination and correctness for two unification algorithms, written in a recursive descent style. One computes unifiers for first order terms, the other for nominal terms (terms including α-equivalent binding structure). Both alg Show more