Lógica parcial trivalorada. Aproximaciones de primer orden, de orden superior e intuicionista

• Autores: Paqui Lucio
• Directores de la Tesis: Mario Rodríguez Artalejo (dir. tes.)
• Lectura: En la Universidad Complutense de Madrid ( España ) en 1994
• Idioma: español
• Tribunal Calificador de la Tesis: Antonio Vaquero Sánchez (presid.) , Javier Leach (secret.) , Luis Fariñas del Cerro (voc.) , Fernando Orejas Valdés (voc.) , Francesc Esteva i Massaguer (voc.)
• Texto completo no disponible (Saber más ...)
• Resumen

  • SE EXTIENDE LA LOGICA DE PRIMER ORDEN CLASICA, DE FORMA CONSERVADORA, A UNA LOGICA TRIVALORADA PL CORRECTA Y COMPLETA CON RESPECTO A UNA SEMANTICA FORMALMENTE DEFINIDA, PL PERMITE EL RAZONAMIENTO ACERCA DE FUNCIONES PARCIALES NO ESTRICTAS DE PRIMER ORDEN, Y ACERCA DEL GRADO DE DEFINICION DE OBJETOS DE TIPO BASICO, LO QUE, EN PARTICULAR, PERMITE EL RAZONAMIENTO ACERCA DE GENEROS CON OBJETOS INFINITOS. PL ES EXTENDIDA, POR EXTENSION SIMPLE, A UNA LOGICA TRIVALORADA DE ORDEN SUPERIOR HOPL. HOPL INCORPORA UN -CALCULO SIMPLEMENTE TIPIFICADO, Y ES CORRECTA Y COMPLETA CON RESPECTO A UNA SEMANTICA DE PRIMER ORDEN BASADA EN LA NOCION DE -MODELO. HOPL PERMITE RAZONAR ACERCA DE FUNCIONES PARCIALES NO ESTRICTAS DE CUALQUIER ORDEN, Y DEL GRADO DE DEFINICION DE OBJETOS FUNCIONALES DE CUALQUIER ORDEN. TANTO PL COMO HOPL SON DOTADAS DE SENDOS METODOS DE TABLEAUX REFUTACIONALMENTE CORRECTOS Y COMPLETOS. ADEMAS DICHOS METODOS DE TABLEAUX SIRVEN DE BASE A UNA METODOLOGIA QUE NOS PERMITE OBTENER CALCULOS DE SECUENCIAS CORRECTOS Y COMPLETOS. SE DISEÑAN CALCULOS DE SECUENCIAS, PARA PL Y HOPL, CON UNA UNICA REGLA NO ACEPTABLE DESDE EL PUNTO DE VISTA INTUICIONISTA (LA REGLA DE REDUCCION AL ABSURDO).

    SE MUESTRA COMO PL Y HOPL PUEDEN SER UTILIZADAS PARA ESPECIFICAR Y PROBAR PROPIEDADES DE TIPOS DE DATOS LIBREMENTE GENERADOS POR CONSTRUCTORAS DE PRIMER ORDEN, DANDO UN ESQUEMA GENERAL DE ESPECIFICACION QUE CARACTERIZA AL MODELO INICIAL DE UN CONJUNTO DE INECUACIONES DESCRIBIENDO LAS CONDICIONES DE ESTRICTICIDAD DE SUS CONSTRUCTORAS. SE DEFINE UNA SEMANTICA INTUICIONISTA ESTILO-KRIPKE CON RESPECTO A LA CUAL LA LOGICA IPL, QUE SE OBTIENE ELIMINANDO EN PL LA REGLA DE REDUCCION AL ABSURDO ES CORRECTA Y COMPLETA. SE FORMULA UN METODO DE TABLEAUX INTUICIONISTAS REFUTACIONALMENTE CORRECTO Y COMPLETO PARA IPL. BASANDOSE EN EL, SE PRUEBA LA COMPLETITUD DEL CALCULO INTUICIONISTA. SE FORMULA UN METODO GENERAL PARA PROBAR CUANDO UNA LOGICA ES EXTENSION (EN SU CASO,