Algoritmos de unificación ecuacional en teorías xerais

Autores: Luis Cachafeiro Chamosa
Directores de la Tesis: José Luis Freire Nistal (1943-) (dir. tes.)
Lectura: En la Universidade da Coruña ( España ) en 1994
Idioma: español
Número de páginas: 219
Tribunal Calificador de la Tesis: José Luis Maté Hernández (presid.) , Antonio Blanco Ferro (secret.) , Juan Pazos Sierra (voc.) , José Alberto Jaén Gallego (voc.) , Miguel López López (voc.)
Enlaces
- Tesis en acceso abierto en: RUC
Resumen
- 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.