Coloquio Mensual del IMERL
Este evento es convocante para el martes 29 de julio a las 16:00 horas, en la Sala de Seminarios del IMERL.
Expositor: Prof. Alexandre Miquel
Título: El Teorema de eliminación de cortes y sus aplicaciones
Resumen: En matemática, hay pruebas directas, en que el razonamiento
sólo usa ingredientes que aparecen en el enunciado demostrado,
y pruebas indirectas (en general mucho más profundas) que
involucran nociones y resultados alejados al enunciado demostrado.
En 1935, el matemático alemán Gerhard Gentzen (1909-1945) introdujo
el cálculo de secuentes, un formalismo que permite representar las
demostraciones matemáticas. Dicho formalismo introduce una regla
de deducción específica ─la regla de corte─, que sirve para introducir
«desvíos» en la demostración, usando argumentos y símbolos intermedios
que no aparecen en el enunciado demostrado. Sin embargo, Gentzen demostró
que la regla de corte es redundante en el cálculo de secuentes, de tal modo
que todo enunciado que tiene una demostración (posiblemente con cortes)
también tiene una demostración sin cortes, es decir: una demostración directa,
pero en general (muchísimo) más larga.
En esta charla, presentaremos y demostraremos el teorema de eliminación de cortes,
así como unas de sus aplicaciones, como el teorema de interpolación de Lyndon.
También hablaremos de las aplicaciones informáticas, como la búsqueda automática de
prueba y la extracción de programas.