Higher-order unification

Posted by rwallace on Stack Overflow See other posts from Stack Overflow or by rwallace
Published on 2009-12-20T17:39:24Z Indexed on 2010/03/23 23:23 UTC
Read the original article Hit count: 405

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?

© Stack Overflow or respective owner

Related posts about unification

Related posts about logic