Leach Albert, JavierNieva Soto, Susana2023-06-192023-06-1920155300098029https://hdl.handle.net/20.500.14352/38676Tesis Universidad Complutense de Madrid,Facultad de Matemáticas, Departamento de Informática y Automática, leída en Madrid, el 1 de junio de 1992; Dirigida por Javier Leach Albert.En la primera parte de la memoria se presenta una logica computacional, que es una logica de predicados con igualdad extendida con polimorfismo y recursion, junto con un sistema de deduccion natural, para esta logica se da una definicion precisa de su semantica y se demuestran buenas propiedades. Se comprueba que es adecuada para razonar acerca de funciones parciales, minimo punto fijo de funcionales y semantica denotacional, y para hacer demostraciones matematicas. Se presenta tambien una extension de los tableaux de Shullyan de primer orden que supone el uso de arboles w-ramificados e instancias monomorfica de las formulas de partida. El algoritmo de los tableaux se utiliza como guia en la construccion de calculos completos. Utilizndo esta propiedad se construye un sistema de reglas de deduccion natural y se prueba que como todo calculo ...spadoctoral thesisopen access510.6(043.2)Lógica simbólica y matemáticaMatemáticas (Matemáticas)Lógica simbólica y matemática (Matemáticas)12 Matemáticas1102.14 Lógica Simbólica