Estou trabalhando em um provador de teoremas de ordem superior, dos quais a unificação parece ser o subproblema mais difícil.

Se o algoritmo de Huet ainda é considerado o estado da arte, alguém tem algum link para explicações dele que são escritas para serem entendidas por um programador ao invés de um matemático?

Ou até mesmo alguns exemplos de onde funciona e o algoritmo de primeira ordem usual não?