PSPACE-Complet, Calcul des séquents, Preuves non bien-Fondées, Preuves circulaires, Coinduction, Recherche de preuves, Logique linéaire, MuMALL, Finitisation

Dans le cadre des logiques adaptées aux plus petits et plus grands points fixes de formules, les preuves circulaires ont été proposées comme alternative aux principes d'induction et coinduction à invariants explicites. Ces preuves circulaires ont reçu un intérêt grandissant ces dernières années avec le développement simultané de leurs applications et de leur méta-théorie. Les preuves infinies sont maintenant bien implantées dans plusieurs sujets de la théorie de la démonstration tels que les prédicats inductifs à la Martin-Löf, la logique linéaire étendue avec des points fixes, etc. Dans le cadre des preuves circulaires ou infinies, non bien-fondées, un critère de validité est nécessaire pour rétablir la cohérence logique. Ce critère sert à distinguer, parmi l'ensemble des prépreuves infinies ou circulaires, celles qui sont des preuves valides. Une approche maintenant standard est de considérer qu'une prépreuve est valide si chacune de ses branches infinies est justifiée par un thread qui progresse infiniment souvent. Cette thèse étudie ces problèmes dans le cadre plus spécifique de MALL étendue avec des points fixes. On sait que, étant donnée une représentation circulaire finie d'une prépreuve non bien-fondée, il est possible de décider en espace polynomial si cette prépreuve est valide vis-à-vis du critère de threads. La première contribution de cette thèse est de démontrer que ce problème de décider le critère de threads pour mu-MALL-omega est en fait PSPACE-complet. Notre démonstration est fondée sur une étude approfondie des liens entre le critère de threads et le principe de size-change termination, habituellement utilisé pour garantir la terminaison de programmes. La deuxième contribution de cette thèse est de décrire un nouveau fragment de l'ensemble des représentations circulaires valides de prépreuves, fondé sur un critère de validité plus contraignant. Ce nouveau critère s'appuie sur un étiquetage des formules et des preuves, et sa validité est purement locale. Il permet à ce fragment d'être plus simple à manipuler, tout en restant suffisamment expressif pour contenir l'image des preuves finitaires du système mu-MALL de David Baelde, qui fonctionnent avec des invariants explicites d'induction et de coinduction. En particulier, il est possible de décider efficacement la validité d'une prépreuve circulaire vis-à-vis de ce nouveau critère, et de calculer efficacement un étiquetage qui certifie cette validité. De plus, et ceci constitue la troisième contribution de cette thèse, la conjecture de Brotherston-Simpson est vraie pour ce fragment : nous décrivons une méthode qui permet de transformer toute preuve circulaire étiquetée de notre fragment en une preuve finitaire, avec des invariants d'induction et de coinduction explicites. Finalement, nous explorons des manières d'étendre ces résultats de validité et de finitisation à un plus grand fragment, en relâchant les contraintes de l'étiquetage tout en conservant (1) la possibilité de certifier localement la validité des preuves et (2) dans une certaine mesure, la possibilité de finitiser les preuves circulaires ainsi étiquetées. (Et plutôt que de nous demander de tout écrire en ASCII, vous pourriez gérer l'UTF8 ?... :-) )