Automating the Derivation of Unification Algorithms: A Case Study in Deductive Program Synthesis
Este artigo apresenta uma derivação totalmente automática de um algoritmo de unificação de três argumentos usando síntese de programas dedutiva, generalizando e automatizando uma prova manual de Manna e Waldinger para gerar um programa correto que computa unificadores idempotentes mais gerais em relação a uma substituição de ambiente acumulante.