Higher-order unification examples
This module presents an encoding of Hilbert's Tenth Problem into
the problem of determining if flexible-flexible disagreement pairs
have closed solutions (assuming that not all types are know to be
This module implements the unification problems that Huet used to show
that third order unification is undecidable. This is done by reducing
the Post correspondence problem to third order unification.