Higher-order unification examples

Higher-order unification examples

Higher-order unification:

hilbert.mod: 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 empty).
post.mod: 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.