La thèse porte sur la logique linéaire, particulièrement à travers l'étude de l'égalité des preuves et de l'équivalence des formules. Cette logique est un raffinement de la logique classique : aussi expressive mais avec des propriétés plus riches. Elle admet une syntaxe de preuves sous la forme de graphes : les réseaux de preuve.
Le principal résultat de cette thèse est la caractérisation des isomorphismes pour le fragment multiplicatif-additif de la logique linéaire (MALL). Deux formules sont isomorphes s'il existe deux preuves les reliant et dont les compositions soient calculatoirement égales à l'identité. Nous avons déterminé un système d'équations qui génère exactement toutes les paires de formules isomorphes, étendant ainsi un résultat par Balat et Di Cosmo pour le fragment multiplicatif (MLL). Les réseaux de preuve de MALL définis par Hughes et van Glabbeek jouent un rôle crucial dans cette preuve. Une caractérisation des rétractions (généralisation des isomorphismes) des formules atomiques est également donnée pour MLL. Afin de démontrer ces résultats, un résultat intermédiaire de confluence du calcul des séquents, à commutation des règles près, a été prouvé.
Un autre résultat est une preuve simplifiée du théorème de séquentialisation des réseaux de Hughes et van Glabbeek, reliant les réseaux de preuve aux arbres de preuve du calcul des séquents.
Elle s'appuie sur une généralisation du théorème de Yeo sur les graphes colorés.
La dernière partie de cette thèse porte sur la formalisation en Coq des réseaux de preuve multiplicatifs. En particulier, la preuve de séquentialisation a été implémentée, ainsi qu'une preuve d'admissibilité de la coupure.
English version
This thesis studies equality of proofs and equivalence of formulas in linear logic. A major tool to this end is the syntax of proof-nets : graphs providing a more canonical representation of proofs than proofs of sequent calculus. We characterize isomorphisms in the multiplicative-additive fragment of linear logic.
Two formulas are isomorphic if they are related with two proofs whose compositions are computationaly equal to the identity, formalizing that these formulas represent the same underlying object. A set of equations generating exactly all isomorphisms is given, extending a result of Balat and Di Cosmo for the multiplicative fragment. Proof-nets from Hughes & van Glabbeek were central in this proof. Another result is a simple proof of sequentialization, linking proof-nets with the usual proofs of sequent calculus.
This proof is deduced from a new generalization of Yeo’s theorem about colored graphs. Lastly, multiplicative proof-nets have been formalized in Coq, along with the above proof of sequentialization and a proof of cut admissibility.
Gratuit
Disciplines