Estoy trabajando en un generador de teoremas de orden superior, de los cuales la unificación parece ser el subproblema más difícil.

Si el algoritmo de Huet todavía se considera de vanguardia, ¿alguien tiene algún vínculo a las explicaciones de éste que estén escritas para que las entienda un programador en lugar de un matemático?

¿O incluso algún ejemplo de dónde funciona y el algoritmo habitual de primer orden no?