000134459 001__ 134459 000134459 005__ 20240424142048.0 000134459 037__ $$aTAZ-TFG-2023-3695 000134459 041__ $$aspa 000134459 1001_ $$aPaesa Lía, Carlos 000134459 24200 $$aFormal logic, automatic theorem checking and proof assistants 000134459 24500 $$aLógica formal, verificación automática de teoremas y asistentes de demostración 000134459 260__ $$aZaragoza$$bUniversidad de Zaragoza$$c2023 000134459 506__ $$aby-nc-sa$$bCreative Commons$$c3.0$$uhttp://creativecommons.org/licenses/by-nc-sa/3.0/ 000134459 520__ $$aEn 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. <br /><br /> 000134459 521__ $$aGraduado en Matemáticas 000134459 540__ $$aDerechos regulados por licencia Creative Commons 000134459 700__ $$aMarco Buzunámiz, Miguel Ángel$$edir. 000134459 7102_ $$aUniversidad de Zaragoza$$bMatemáticas$$cGeometría y Topología 000134459 8560_ $$f798974@unizar.es 000134459 8564_ $$s320304$$uhttps://zaguan.unizar.es/record/134459/files/TAZ-TFG-2023-3695.pdf$$yMemoria (spa) 000134459 909CO $$ooai:zaguan.unizar.es:134459$$pdriver$$ptrabajos-fin-grado 000134459 950__ $$a 000134459 951__ $$adeposita:2024-04-24 000134459 980__ $$aTAZ$$bTFG$$cCIEN 000134459 999__ $$a20230903130711.CREATION_DATE