Higher-order unification
- by rwallace
I'm working on a higher-order theorem prover, of which unification seems to be the most difficult subproblem.
If Huet's algorithm is still considered state-of-the-art, does anyone have any links to explanations of it that are written to be understood by a programmer rather than a mathematician?
Or even any examples of where it works and the usual first-order algorithm doesn't?