Teorema de corte-eliminación
Cut-elimination
- Fecha
- 1935 · fiabilidad alta
- Lugar
- Gotinga, Alemania
- Autoría
- Gerhard Gentzen
- Ámbito
- Saber y símbolos
Qué se descubrió
El teorema de corte-eliminación (Hauptsatz de Gentzen) es el resultado central que sustenta la relevancia del cálculo de secuentes: establece que toda sentencia demostrable usando la regla de corte también posee una demostración que prescinde de ella. Lo probó Gerhard Gentzen en 1935 para los sistemas LJ y LK de lógica intuicionista y clásica.
A qué dio paso
- Fundamento de la teoría de la demostración moderna
- Base de la correspondencia Curry-Howard y la programación funcional tipada
- Aplicación en la verificación automática de demostraciones