Eliminación de Cortes

Un procedimiento en teoría de la demostración que transforma una prueba en cálculo de secuentes (o deducción natural) para eliminar las inferencias de corte (aplicaciones de la regla 'cut'), produciendo una prueba libre de cortes que típicamente satisface la propiedad de subfórmula.

La transformación de prueba que elimina las inferencias de corte (aplicaciones de la regla cut) de una prueba en estilo cálculo de secuentes para producir una derivación sin cortes del mismo secuente final, preservando la demostrabilidad aunque a menudo cambiando la estructura y el tamaño de la prueba.