Una lógica trivalorada para funciones recursivas parciales

Laburpena

EL OBJETIVO DE LA TESIS ES DAR UNA NUEVA FUNDAMENTACION LOGICA A LAS FUNCIONES PARCIALES COMPUTABLES, EN EL CAPITULO PRIMERO SE INTRODUCE UN NUEVO VALOR BOOLEANO INDEFINIDO CON EL QUE SE EXTIENDEN LAS NOCIONES CLASICAS DE VALOR DE UNA FORMULA Y DE CONSECUENCIA LOGICA. EN EL CAPITULO SEGUNDO SE PRESENTA LA LOGICA LFP (LOGICA DE PRIMER ORDEN PARA FUNCIONES PARCIALES CON TERMINOS CONDICIONALES), Y SE ESTUDIA LA COMPLETITUD DE LOS CALCULOS DE SECUENCIAS DE ESTA LOGICA POR EL METODO DE LOS TABLEAUX CON LA CONSTRUCCION DE UN MODELO "AL ESTILO DE HINTIKKA". EN EL CAPITULO TERCERO SE EXTIENDE LFP A LFRP (LOGICA DE PRIMER ORDEN PARA FUNCIONES RECUSRIVAS PARCIALES). SE EMPLEA EL METODO DE LOS TABLEAUX PARA OBTENER CONDICIONES DE COMPLEETITUD DE UN MODO SEMEJANTE AL DEL CAPITULO ANTERIOR. EN ESTE CASO LOS CALCULOS SON INFINITARIOS Y LA LOGICA PIERDE UNA PROPIEDAD IMPORTANTE DE LA LOGICA DE PRIMER ORDEN AL NO SATISFACER EL TEOREMA DE FINITUD. EN EL CAPITULO CUARTO SE APLICA LFRP AL ESTUDIO DE LA SEMANTICA DE UN LENGUAJE IMPERATIVO, DE TIPO ALGOL, Y SE MUESTRA COMO LFRP TIENE TANTA POTENCIA EXPRESIVA COMO OTRAS LOGICAS USADAS PARA PROGRAMAS IMPERATIVOS.