Jérôme Fortier, La règle de coupure dans les preuves circulaires

Programme

Résumé

Les preuves circulaires, dans lesquelles certaines conclusions peuvent être démontrées à partir d’elles-mêmes, furent introduites dans [1] pour étudier la calculabilité dans les modèles du μ-calcul, soit avec les opérations suivantes : produits et coproduits finis, algèbres initiales et coalgèbres terminales. Le calcul en question, sans règle de coupure, était correct et complet, mais pas plein, c’est-à-dire qu’il ne représentait pas toute la structure des modèles catégoriques visés.

On remplit donc le système de preuves circulaires en introduisant la règle de coupure. La nouvelle syntaxe permet une procédure d’élimination des coupures qui produit un arbre infini, modélisant ainsi le calcul recherché.

Plusieurs directions de recherche en découlent, qui sauront, on l’espère, intéresser autant les logiciens que les informaticiens !

[1] L. Santocanale, A calculus of circular proofs and its categorical semantics, in : M. Nielsen, U. Engberg (eds.), FOSSACS 2002, No. 2303 in LNCS, Springer, 2002.