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

• Autores: Gabriel Aguilera Venegas
• Directores de la Tesis: Inmaculada Pérez de Guzmán Molina (dir. tes.)
• Lectura: En la Universidad de Málaga ( España ) en 1997
• Idioma: español
• Tribunal Calificador de la Tesis: Francisco Andrés Triguero Ruiz (presid.) , Juan José Saameño Rodríguez (secret.) , José María Barja Pérez (voc.) , José Juan Quesada Molina (voc.) , Eduardo Medina Cano (voc.)
• Enlaces
  • Tesis en acceso abierto en: www.sci.uma.es (pdf)
• Resumen

  • 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++.