Resumen de Una teoría computacional acerca de la lógica ecuacional (formalización en acl2 de la lógica ecuacional y demostración automática de sus propiedades)
El objetivo principal de la Tesis es el desarrollo de una teoria computacional acerca de la logica ecuacional, usando para ello el sistema ACL2, Es decir, se usa ACL2 para definir formalmente algoritmos y conceptos relacionados con la lógica ecuacional, y se llevan a cabo demostraciones automáticas de teoremas acerca de estos algoritmos y conceptos. Este trabajo de verificación formal se realiza en un entorno en el que se pueden combinar la demostración de teoremas con la ejecución de funciones.
La teoria desarrollada se estructura en tres bloques:
-Propiedades de los terminos de primer orden y su estructura de reticulo respecto de la relacion de subsuncion.
-Reducciones abstractas.
-Teorias ecuacionales y sistemas de reescritura de terminos De entre los teoremas demostrados automáticamente cabe destacar la verificacion formal de un algoritmo de unificacion, el lema de Newman para reducciones abstractas y el teorema de pares criticos de Knuth y Bendix.
