Tesis doctoral de José Luis Ruiz Reina
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.
Datos académicos de la tesis doctoral «Una teoria computacional acerca de la logica ecuacional (formalizacion en acl2 de la logica ecuacional y demostracion automatica de sus propiedades)«
- Título de la tesis: Una teoria computacional acerca de la logica ecuacional (formalizacion en acl2 de la logica ecuacional y demostracion automatica de sus propiedades)
- Autor: José Luis Ruiz Reina
- Universidad: Sevilla
- Fecha de lectura de la tesis: 28/09/2001
Dirección y tribunal
- Director de la tesis
- José Antonio Alonso Jimenez
- Tribunal
- Presidente del tribunal: Luis María Laita de la rica
- robert lukas mario Nieuwenhuis (vocal)
- alejandro Fernandez margarit (vocal)
- albert Rubio gimeno (vocal)