RT Dissertation/Thesis
T1 Una lógica computacional con polimorfismo y recursión y un sistema de deducción automática basado en ella
A1 Nieva Soto, Susana
AB 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 ...
PB Universidad Complutense de Madrid
YR 2015
FD 2015
LK https://hdl.handle.net/20.500.14352/38676
UL https://hdl.handle.net/20.500.14352/38676
LA spa
NO Tesis 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.
NO ProQuest
DS Docta Complutense
RD 21 abr 2026