| TAZ-TFG-2023-3695 |
Lógica formal, verificación automática de teoremas y asistentes de demostración
Paesa Lía, Carlos
Marco Buzunámiz, Miguel Ángel (dir.)
Universidad de Zaragoza,
CIEN,
2023
Departamento de Matemáticas, Área de Geometría y Topología
Graduado en Matemáticas
Resumen: En este trabajo buscamos dar una explicación sobre cómo formalizar el razonamiento lógico, cómo este se relaciona con la teoría de tipos y cómo los asistentes de demostración pueden ser utilizados para la verificación automática de teoremas. En el primer capítulo definimos el concepto de sistema formal y trabajamos con el ejemplo más básico: la lógica proposicional. En el segundo extendemos las nociones vistas en el primero para demostrar el teorema de Completitud de Gödel y otras propiedades interesantes de la lógica de primer orden, acabando con una introducción a sistemas de orden superior. El último capítulo introduce brevemente los conceptos centrales de la teoría de tipos para poder explicar la correspondencia de Curry-Howard entre modelos de computación (teoría de tipos) y los sistemas formales de los que hablamos en los otros capítulos.
Tipo de Trabajo Académico: Trabajo Fin de Grado
Enlace permanente:
El registro pertenece a las siguientes colecciones:
Trabajos académicos > Trabajos Académicos por Centro > Facultad de Ciencias
Trabajos académicos > Trabajos fin de grado