Tesis doctoral de Gabriel Aguilera Venegas
Esta tesis estudia la demostracion automatica de teoremas en logicas trivaluadas. Concretamente se presenta un demostrador denominado tas-m3 para la logica trivaluada completa m3. Esta tesis cuenta con una orientacion a las aplicaciones y es de gran importancia la forma en la que se genera el modelo para la negacion de la formula de entrada. Es un metodo que no esta basado en resolucion y por tanto no adolece de las deficiencias de este metodo (poca interaccion con el ser humano, dificultad de obtener formas normales en logicas no clasicas, etc.). ademas de la demostracion de correccion y completitud del metodo se demuestran otros teoremas relacionados con los procesos. El trabajo se complementa con un estudio comparativo con los metodos actualmente mas utilizados. tambien se añaden capitulos en los que se introducen los conceptos que se utilizan a lo largo del trabajo asi como un capitulo dedicado a las logicas multivaluadas. Se añade un apendice en el que se resume el demostrador para la logica clasica tas-d al que se le incorporan las mejoras que el estudio del caso multivaluado ha motivado. en la exposicion y defensa se utiliza una implementacion del metodo para entornos graficos realizada en c++.
Datos académicos de la tesis doctoral «Reducciones totales y parciales para el analisis de validez y construccion de modelos en m3.«
- Título de la tesis: Reducciones totales y parciales para el analisis de validez y construccion de modelos en m3.
- Autor: Gabriel Aguilera Venegas
- Universidad: Málaga
- Fecha de lectura de la tesis: 01/01/1997
Dirección y tribunal
- Director de la tesis
- Inmaculada Perez De Guzman Molina
- Tribunal
- Presidente del tribunal: Francisco Triguero Ruiz
- Juan Quesada Molina (vocal)
- Barja Perez José María (vocal)
- Eduardo Medina Cano (vocal)