Le but de cette thèse est de fournir un système de preuves structurelles pour la logique modale de Riesz. La logique modale de Riesz est une logique modale à valeurs réelles, i.e., ces termes sont interprétés par des nombres réels plutôt que par des Booléens. De plus, la logique modale de Riesz étendue avec des opérateurs (co)inductifs est suffisamment expressive pour encoder la plupart des logiques probabilistes classiques. L'objectif de fournir un calcul des hypersequents pour la logique modale de Riesz est d'avoir un système de preuve à la fois correct et complet, et dont toutes les règles sont analytiques (informellement, nous ne voulons pas qu'ils soient nécessaire de deviner des termes pour produire une dérivation).
Pour ce faire, nous étendons le calcul des hypersequents introduit par Gab- bay, Metcalfe et Olivetti pour la logique Abélienne. La logique modale de Riesz peut être vue comme la logique Abélienne étendue avec la multiplication par un nombre réel et un opérateur modal. Nous avons donc rajouté des règles pour ces nouvelles opérations, ce qui a nécessité des modifications importantes sur la structure des hypersequents que nous considérons, et donc sur les preuves des résultats clés. Nous avons prouvé que notre calcul des hypersequents était complet et correct pour la logique modale de Riesz. Nous avons également utilisé ce système pour prouver des résultats nouveaux : nous avons prouvé que la logique modale de Riesz était décidable et nous avons répondu à un problème ouvert sur son axiomatisation.
Gratuit
Disciplines