[PhD position 2021] Sémantique, Preuves et Réfutations en Logiques de Ressources.

Mots clés: sémantique, théorie de la preuve, transformation de preuves, réfutations, logiques de ressources.

Contact

Didier GALMICHE (galmiche@loria.fr)

Daniel MERY (dmery@loria.fr)

Résumé

Dans cette thèse, nous nous concentrons sur des extensions et variantes de BI, la logique des implications en buissons, qui est une combinaison de la logique intuitionniste (IL) et de la logique linéaire multiplicative intuitionniste (MILL). BBI, la variante booléenne de BI, est le noyau logique à partir duquel les logiques spatiales et de séparation sont construites.

Nous nous intéresserons :
– à l’étude de transformations de preuves entre calculs avec et sans labels pour les logiques de ressources de la famille de BI,
– à la proposition de nouvelles sémantiques de ressources,
– à la conception d’algorithmes effectifs de résolution de contraintes d’accessibilité dans les graphes de ressources,
– à la définition de systèmes de réfutation.

Contexte scientifique

Les systèmes informatiques modernes sont devenus hautement complexes et impliquent une multitude d’interactions entre une grande variété de composants hétérogènes qui peuvent être vus comme des ressources. Ces systèmes gagnant plus de contrôle sur de nombreux aspects de la vie humaine (par exemple, le trafic aérien, les réseaux bancaires et sociaux), il devient également plus important de s’assurer de leur correction, soit a priori par conception, ou a posteriori par vérification.

La notion de ressource est une notion de base dans de nombreux domaines incluant l’économie, l’ingénierie et la psychologie, mais c’est probablement dans le domaine informatique qu’elle est mise le plus distinctement en lumière. Les ressources peuvent être physiques (comme une imprimante ou un processeur) ou abstraites (comme un programme ou une fonction mathématique), elles peuvent être statiques (comme un jeton dans un réseau de Petri) ou dynamiques (c’est à dire, évoluant par elles-mêmes tel un processus ou un thread).

L’étude des problèmes soulevés par les ressources et leur gestion dans un cadre formel bien défini est le but des logiques de ressources et de leurs sémantiques de ressources associées. Par exemple, les logiques linéaires traitent d’aspects liés au partage et à la consommation de ressources, tandis que les logiques de séparations traitent d’aspects liés au partage et à la séparation. Les logiques modales et d’ambiance sont quant à elles bien adaptées aux problèmes impliquant la distribution spatiale et temporelle des ressources ainsi que leur mobilité.

Sujet et objectifs

Dans cette thèse, nous nous concentrons sur des extensions et variantes de BI, la logique des implications en buissons [9], qui est une combinaison de la logique intuitionniste (IL) et de la logique linéaire multiplicative intuitionniste (MILL). BBI, la variante booléenne de BI [4], est le noyau logique à partir duquel les logiques spatiales et de séparation sont construites.

Il existe de nombreux calculs pour BI. Les plus remarquables sont le calcul des séquents purement syntaxique LBI [9] et les calculs à base de tableaux/séquents avec labels TBI/GBI [3,6]. La traduction des preuves de LBI en preuves de TBI/GBI est bien connue. De manière surprenante, la traduction des preuves de TBI/GBI en preuves de LBI est loin d’être triviale et reste encore un problème ouvert à ce jour malgré des avancées récentes pour une petite sous-classe de preuves de GBI n’ayant qu’une seule formule à droite (preuves de sGBI) et vérifiant une propriété d’arbre très spécifique [6].

Un premier objectif de cette thèse est d’étendre les résultats précédents aux preuves de GBI avec plusieurs formules à droite (preuves de mGBI) et d’étudier la possibilité de normaliser des preuves arbitraires de mGBI en preuves de mGBI satisfaisant la propriété d’arbre.

Même dans le cas plus simple de IL, la traduction de preuves avec labels vers des preuves en séquents sans labels reste un problème non trivial qui nécessite une étape de traduction intermédiaire passant par la logique bi-intuitionniste (biInt) [8]. La logique bi-intuitionniste [1] est une extension de IL dans laquelle un nouveau connecteur appelé co-implication est ajouté. BiInt peut être vue comme une logique combinant IL, qui favorise une notion de vérification constructive (c’est à dire, la prouvabilité), avec la logique intuitionniste duale (DualInt), qui favorise une notion de falsification constructive (c’est à dire, la réfutabilité). La dualité preuves/réfutations a été capturée avec succès dans les jeux dialogiques de Lorenzen où un joueur essaie de prouver une formule tandis que l’autre essaie de la réfuter [2].

Un second objectif de cette thèse est de concevoir une extension bi-intuitionniste de la logique BI et de déterminer si une telle extension pourrait servir d’étape intermédiaire pour des traductions plus générales des preuves de GBI vers les preuves de LBI.

Dans nos travaux sur les calculs avec labels pour BI [3] et BiInt [8] nous avons mis en évidence l’importance de structures, appelées graphes de ressources, qui capturent la validité d’une formule en termes de contraintes d’accessibilité entre labels. Les graphes de ressources sont utilisés à la fois comme guides pour la recherche de preuves et pour l’extraction de contre-modèles [3] en cas de non prouvabilité. La construction de contre-modèles est centrale dans notre approche car il est essentiel dans la pratique quotidienne de comprendre rapidement pourquoi une spécification échoue quand elle échoue. Pour le moment, nous disposons d’algorithmes effectifs de résolution de contraintes pour les graphes de ressources de BiInt [5], dans lesquels les labels sont atomiques et peuvent contenir des variables libres, et pour les graphes de ressources de BI, dans lesquels les labels sont des chaînes de caractères sans variables libres.

Un troisième objectif de cette thèse est de proposer et d’implémenter des algorithmes effectifs de résolution de contraintes pour des cas plus généraux de graphes fabriqués à partir de labels non atomiques pouvant contenir des variables libres.

Un contre-modèle est un objet sémantique témoignant de la non validité d’une formule dans une sémantique donnée, tandis qu’une réfutation est un objet syntaxique témoignant de la non prouvabilité d’une formule dans un système de preuve donné. Par exemple, CRIP est un système de réfutation pour IL [7]. En l’absence d’un théorème de complétude, réfutations et contre-modèles ne coïncident pas forcément. De plus, un contre-modèle peut être difficile à construire et encore plus à interpréter (ce qui réduit grandement son intérêt pratique) lorsque la sémantique sous-jacente est trop abstraite ou trop élaborée (comme, par exemple, la sémantique à base de topologies de Grothendieck pour BI). Dans une telle situation, construire une réfutation plutôt qu’un contre-modèle semble préférable. Actuellement, il n’existe aucun système de réfutation pour les logiques de ressources construites à partir du noyau logique de BI.

Un quatrième objectif de cette thèse est donc d’explorer la question et de proposer si possible des systèmes de réfutation pour la famille des logiques de ressources issues de BI.

Références

[1] T. Crolard. Subtractive logic. In Theoretical Computer Science, 254(1-2) :151–185, 2001.

[2] W. Felscher. Dialogues, strategies, and intuitionistic provability. In Annals of Pure and Applied Logic, 28(3):217–254, 1985.

[3] D. Galmiche, D. Méry, and D. Pym. The semantics of BI and Resource Tableaux. Mathematical Structures in Computer Science, 15(6) :1033–1088, 2005.

[4] D. Galmiche and D. Larchey-Wendling. Expressivity properties of Boolean BI through relational models. In Int. Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2006, LNCS 4337, pages 357–368, Kolkata, India, 2006.

[5] D. Galmiche and D. Méry. A connection-based characterization of bi-intuitionistic validity. In Int. Conference on Automated Deduction, CADE 23, LNCS 6803, pages 268–282, Wroclaw, Poland, 2011.

[6] D. Galmiche, M. Marti and D. Méry. Relating labelled and label-free bunched calculi in BI logic. In 28th Int. Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2019, LNCS 11714, pages 130–146, London, United Kingdom, 2019.

[7] L. Pinto and R. Dyckhoff. Loop-free construction of counter-models for intuitionistic propositional logic. In Symposia Gaussiana, Conference A, pages 226–232, 1995.

[8] L. Pinto and T. Uustalu. Relating sequent calculi for bi-intuitionistic propositional logic. In 3rd Workshop on Classical Logic and Compution, CL&C 2010, EPTCS 47, pages 57–72, Brno, Czech Republic, 2010.

[9] D. Pym. The Semantics and Proof Theory of the Logic of Bunched Implications, volume 26 of Applied Logic Series. Kluwer Academic Publishers, 2002.

Équipe d’accueil

La thèse est proposée par l’équipe TYPES du laboratoire de recherche LORIA.

Compétences et profil

  • Qualifications requises: un Master en Informatique (ou équivalent)
  • Des connaissances dans les domaines suivants seront appréciées: logique, théorie de la preuve, sémantique, programmation (C, CAML, Java, Python)

Informations complémentaires

Durée: 3 ans

Date de début: entre le 1er octobre 2021 et le 1er décembre 2021

Comment candidater

Envoyer les documents suivants à galmiche@loria.fr et dmery@loria.fr

  • un CV
  • une lettre de motivation
  • les certificats et relevés de notes de la Licence et du Master (ou équivalents)

Logo d'Inria