Combinatorial flows
Flux combinatoires
Résumé
In this thesis, we introduce combinatorial flows for proofs in Classical propositional logic as a response to the problem of proof identity and proof comparison which we refer to as the 24th problem of Hilbert. Combinatorial flows are a graphical representation of proofs inspired by properties of atomic flows and combinatorial proofs. From atomic flows, introduced by Guglielemi and Gundersen, they inherit the close correspondence with open deduction, the possibility of tracing the atom occurrences in a derivation, and the free compositionality. From combinatorial proofs, introduced by Hughes, they inherit the correctness criterion that allows the reconstruction of the derivation from the flow and the differentiation between the linear and the resource management part of the proof. In fact, we will show that combinatorial flows form a proof system in the sense of Cook and Reckhow. Moreover, we will show how to translate between derivations from different proof systems (namely natural deduction, sequent calculus, and deep inference) and combinatorial flows, and we will show their relation with combinatorial proofs with cuts. Finally, we will discuss normal forms and normalization procedures on combinatorial flows while introducing purification as a sub-procedure concerned with the presence of units in language.
Dans cette thèse, nous introduisons des flux combinatoires pour les preuves en logique propositionnelle classique, pour répondre au problème de l'identité des preuves et de la comparaison des preuves que nous appelerons le 24ème problème de Hilbert. Les flux combinatoires sont une représentation graphique de preuves inspirés des propriétés des flux atomiques et des preuves combinatoires. Des flux atomiques, introduits par Guglielemi et Gundersen, ils héritent de la correspondance étroite avec la déduction ouverte, de la possibilité de retracer les occurrences des atomes dans une dérivation et de de la compositionnalité libre. Des preuves combinatoires, introduites par Hughes, elles héritent du critère de correction qui permet la reconstruction de la dérivation à partir du flux et la différenciation entre la partie linéaire et la partie gestion des ressources de la preuve. En fait, nous montrerons que les flots combinatoires forment un système de preuve au sens de Cook et Reckhow. De plus, nous établissons une traduction entre les dérivations de différents systèmes de preuve (à savoir la déduction naturelle, le calcul séquentiel et l'inférence profonde) et les flux combinatoires, ainsi que leur lien avec les preuves combinatoires avec coupures. Enfin, nous discuterons des formes normales et des procédures de normalisation sur les flux combinatoires tout en introduisant la purification comme sous-procédure concernée par la présence d'unités dans le langage.
| Origine | Version validée par le jury (STAR) |
|---|