Sistemas de tipos puros con universos
- Autores: Blas Carlos Ruiz Jiménez
- Directores de la Tesis: José María Troya Linero (dir. tes.)
- Lectura: En la Universidad de Málaga ( España ) en 1999
- Idioma: español
- Tribunal Calificador de la Tesis: Juan José Moreno Navarro (presid.) , Ernesto Pimentel Sánchez (secret.) , Inmaculada Pérez de Guzmán Molina (voc.) , Antonio Javier Gavilanes Franco (voc.) , Buenaventura Clares Rodríguez (voc.)
- Texto completo no disponible (Saber más ...)
- Resumen
Los Sistemas de Tipo Puros con Universos propuestos en esta tesis permiten modelar de forma apropiada las teorías de tipos y los sistemas lógicos más interesantes, y constituyen el núcleo de la mayoría de los Marcos Lógicos utilizados en la demostración automática de teoremas, Este trabajo propone tales teorías como generalización de otras teorías desarrolladas por un amplio número de investigadores.
Proporciona un estudio general, del cual se pueden obtener propiedades clásicas de muchos sistemas. Desarrolla un original mecanismo algebraico, que es aplicado en la demostración de algunas propiedades no triviales, como la propiedad de "condensación" o la propiedad "decidibilidad del problema de la comprobación de tipos".
Tales propiedades son caracterizadas a través de un simple concepto de conservación de la tipificación bajo reducciones entre universos generalizados.
Sugiere que las herramientas algebraicas desarrolladas son susceptibles de ser utilizadas para resolver otros problemas de la teoría de tipos hoy día aún abiertos.
