Élimination des Coupures

Une procédure en théorie des preuves qui transforme une preuve en calcul des séquents (ou en déduction naturelle) afin de supprimer les inférences de coupure (applications de la règle 'cut'), produisant une preuve sans coupure satisfaisant typiquement la propriété des sous-formules.

La transformation de preuve qui supprime les inférences de coupure (applications de la règle cut) d'une preuve de style calcul des séquents pour produire une dérivation sans coupure du même séquent final, préservant la démontrabilité tout en modifiant souvent la structure et la taille de la preuve.