Logique linéaire, Réseaux de preuves, Sémantique des phases, Preuves circulaires, Logique à points fixes, Élimination des coupures

Le sujet de cette thèse est la théorie de la preuve de la logique linéaire avec plus petits et les plus grands points fixes. Plusieurs systèmes ont été étudiés dans la littérature pour ce langage : le système bien fondé qui repose sur la règle d'induction de Park, et des systèmes qui caractérisent implicitement l'induction comme le système circulaire et son extension non bien fondée. Cette thèse contribue à la théorie de ces systèmes avec pour but ultime de capturer exactement la relation de prouvabilité de ces systèmes et de permettre l'application de ces objets dans les langages de programmation supportant le raisonnement (co)inductif. Cette thèse contient trois parties. Dans la première partie, nous rappelons la littérature sur la logique linéaire et les principales approches de la théorie de la preuve des logiques à points fixes. Dans la deuxième partie, nous obtenons une sémantique de vérité pour le système bien fondé, nous concevons de nouveaux systèmes infiniment ramifiés bien fondés, et nous calculons la complexité de la prouvabilité dans les systèmes circulaires et non bien fondés. Dans la troisième partie, nous concevons des réseaux de preuves non bien fondés et étudions leur dynamique.