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