| 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
Matemáticas department, Geometría y Topología area
Graduado en Matemáticas
Abstract: 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
Permalink:
El registro pertenece a las siguientes colecciones:
Academic Works > Trabajos Académicos por Centro > facultad-de-ciencias
Academic Works > End-of-grade works