Ciencias de la Computación (plan 2013) 2024-2

Grupo 7127, 20 lugares. 8 alumnos.

 

El objetivo de este curso es estudiar algunos aspectos importantes de la la teoría estructural de la prueba en lógicas no clásicas, en específico lógicas de segundo orden, lógica modal y lógica lineal. Se hará énfasis en sus aplicaciones en Ciencia de la Computación Teórica, en específico estudiando los procesos de normalización y búsqueda de pruebas como nociones de cómputo así como la correspondencia de Curry-Howard y sus aplicaciones en los sistemas de tipos para lenguajes de programación, en particular en cálculos sensibles a recursos (procesos concurrentes)

Prerrequisitos: Este curso es una continuación del Seminario de Introducción a la Teoría de la Prueba que impartí el semestre pasado. Sin embargo será autocontenido y se utilizarán las dos primeras semanas de clases para dar un panorama de los principales resultados del curso anterior. Adicionalmente es deseable haber llevado Lógica Computacional o bien Lógica Matemática II. Una ventaja adicional es haber llevado Lenguajes de Programación.

Para cualquier duda o pregunta sobre el curso pueden escribir a favio@ciencias.unam.mx

Forma de evaluación: mediante ejercicios semanales, tareas examen mensuales y una exposición al final del semestre (calificando documento escrito y presentación ante el grupo)

Temario

1. Introducción y panorama del curso anterior: lógica proposicional y de predicados, Deducción natural (sistemas minimal, intuicionista y clásico). Búsqueda de pruebas en el cálculo de secuentes. Los teoremas de normalización y eliminación de corte. Cálculo lambda y la correspondencia de Curry-Howard.

2. Lógicas de segundo orden (proposicional y de predicados).

3. Lógica modal: sistemas axiomáticos, S4 (deducción natural y sistema de contexto dual), sistemas deductivos etiquetados.

4. Lógica lineal: deducción natural y sistema dual. Correspondencia de Curry-Howard mediante el cálculo pi.

5. Tópicos adicionales (sujeto al tiempo): búsqueda de pruebas en lógica modal y lineal (focusing), semántica mediante teoría de la prueba, realizabilidad.

Bibliografía general (también usaremos artículos y notas que se darán en clase)

Paolo Mancosu, Sergio Galvan, Richard Zach. An Introduction to Proof Theory Normalization, Cut-Elimination, and Consistency Proofs. Oxford University Press 2021.

Sara Negri, Jan von Plato. Structural Proof Theory. Cambridge University Press 2001.

Sara Negri, Jan von Plato. Proof Analysis. Cambridge University Press 2011.

Jan von Plato. Elements of Logical Reasoning. Cambridge University Press 2013.

Morten H. Sorensen, Pawel Urzyczyn. Lectures on the Curry-Howard Isomorphism. Studies in Logic and the Foundations of Mathematics. Vol. 149. Elsevier 2006.

Anne S. Troelstra, Helmut Schwichtenberg. Basic Proof Theory. 2nd Edition. Cambridge University Press 2000.