Reducciones totales y parciales para el análisis de validez y construcción de modelos en M3

Abstract

Esta tesis estudia la demostración automática de teoremas en lógicas trivaluadas. Concretamente se presenta un demostrador denominado tas-m3 para la lógica trivaluada completa m3. Esta tesis cuenta con una orientación a las aplicaciones y es de gran importancia la forma en la que se genera el modelo para la negación de la formula de entrada. Es un método que no está basado en resolución y por tanto no adolece de las deficiencias de este método(poca interacción con el ser humano, dificultad de obtener formas normales en lógicas no clásicas, etc.). Además de la demostración de corrección y completitud del método se demuestran otros teoremas relacionados con los procesos. El trabajo se complementa con un estudio comparativo con los métodos actualmente más utilizados. También se añaden capítulos en los que se introducen los conceptos que se utilizan a lo largo del trabajo así como un capítulo dedicado a las lógicas multivaluadas. Se añade un apéndice en el que se resume el demostrador para la lógica clásica TAS-D al que se le incorporan las mejoras que el estudio del caso multivaluado ha motivado. En la exposición y defensa se utiliza una implementación del método para entornos gráficos realizada en C++.