Le théorème d'élimination des coupures constitue l'un des résultats fondamentaux de la théorie de la démonstration. Il exprime une idée relativement contre-intuitive : sous certaines hypothèses, un système de règles pour une logique donnée est capable de démontrer toutes ses formules valides sans jamais recourir à la règle de coupure (c'est-à-dire, dans ce contexte, une forme de modus ponens). Autrement dit, toute démonstration peut être menée sans introduire de lemmes intermédiaires.


Traditionnellement, la preuve de ce résultat est de nature algorithmique. On définit une procédure de transformation des démonstrations et l'on montre que celle-ci termine toujours sur une preuve dépourvue de coupures.

Dans cet exposé, nous nous intéressons à l'élimination des coupures dans un cadre où les démonstrations peuvent être infinies. Plus précisément, nous étudions ce problème pour l’Alternating-Time Temporal Logic (ATL), une logique largement utilisée pour la vérification des systèmes multi-agents. Les opérateurs stratégiques d’ATL reçoivent une sémantique coinductive, ce qui conduit naturellement à l’apparition d’arbres de preuve potentiellement infinis. Dans ce contexte, l’approche classique fondée sur la terminaison d’une procédure de réécriture ne peut plus être appliquée directement.

Notre contribution consiste à reformuler l’élimination des coupures en termes de convergence. Plutôt que d’exiger qu’une procédure termine après un nombre fini d’étapes, nous montrons que l’application itérée des règles de réécriture converge, dans un sens approprié, vers une démonstration sans coupure. L’élimination des coupures apparaît ainsi comme un processus de passage à la limite, ce qui permet d’étendre ce résultat fondamental de la théorie de la démonstration au cadre coinductif d’ATL.