Resumen de Algoritmos de unificación ecuacional en teorías xerais
Se presenta un nuevo algoritmo universal de E-unificación que es completo en teorías generales, utilizando el esquema de unificación de pares de substituciones, este método es una generalización de Narrowing para conservar la completitud en aquellas teorías para las que este no es completo. Se prueba que es también una especializacion de Relaxed Narrowing (Dougherty y Johann) y se comprueba, mediante una implementación en Caml, que reduce un número considerable de soluciones redundantes y detecta rápidamente la no E-unificabilidad. Se introducen nuevas mejoras en el método y se muestra favorable en la comparación con los otros métodos generales de unificación ecuacional se incorporan los programas en Caml, los resultados y otros resultados originales en este campo.
