El Profesor Alexandre Miquel va a dar
cierre a este ciclo mensual de charlas del Coloquio Mensual del IMERL.
Su charla tendrá lugar el martes 29 de julio a las 16:00
horas, en la Sala de Seminarios del IMERL.
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.