Traduction et Découverte des Calculs pour les logiques Modales et dérivées – TICAMORE

Le projet est fondé sur de la recherche théorique fondamentale et profite des concepts fondamentaux et des techniques de la théorie de la preuve :
- élimination/admissibilité de la coupure : une propriété centrale d'un système de preuves, nécessaire pour assurer son analycité, une condition essentielle pour obtenir des propriétés (terminaison de la recherche de preuves), génération de contre-modèles et méta-propriétés (interpolation).

- analyse sémantique d'une logique : nécessité de définir des calculs avec labels, capturant la sémantique dans la syntaxe de façon contrôlée. Les calculs obtenus peuvent être transformés en calculs internes par normalisation et transformation de preuves.

- analyse des systèmes de preuve pour garantir la terminaison et des bornes de complexité : elle est fondée à la fois sur le contrôle de la recherche de preuves, la détection de redondances, et sur les propriétés standard de théorie de la preuve, comme la permutabilité des règles.

- techniques de transformation de preuves : fondées sur la permutabilité et l'admissibilité des règles en vue d'obtenir des formes normales ayant des propriétés particulières.

- implantation de calculs : sous forme de démonstrateurs de théorèmes intégrant de la recherche de preuves automatisée. En particulier la méthodologie LEAN d'implantation en Prolog conduit à des implantations compactes de calculs. Une alternative est l'utilisation d'assistants de preuve qui permettent de vérifier les preuves et de les construire interactivement.

La recherche est développée suivant trois axes principaux du projet.

TRADUCTIONS ENTRE CALCULS INTERNES ET EXTERNES
Nous avons proposé des traductions constructives entre des calculs pour les principales logiques de ce projet : logiques conditionnelles, logique BI et logique du temps “tense”.

DE NOUVEAUX CALCULS INTERNES A PARTIR DE CALCULS EXISTANTS ET APPLICATIONS
Nous avons étudié de nouveaux calculs internes pour des familles de logiques, soit à partir de calculs externes soit à partir d'une spécification sémantique :
- logiques modales et des conditionnels: les premiers calculs internes pour des logiques des conditionnels complexes, et de nouveaux calculs avec labels pour les logiques modales non-normales.
- logiques BI : un nouveau calcul avec labels pour la logique linéaire multiplicative intuititionniste, le premier calcul des tableaux pour la logique de séparation avec annonces publiques et de nouveaux calculs fondés sur des hypersequents avec bunches.
- logiques intermédiares : le premier système de déduction naturelle pour une large classe de logiques intermédiaires via une traduction entre hypersequents et systèmes de règles de niveau deux.

Application de techniques de théorie de la preuve à la résolution de problèmes ouverts :
- nous avons montré que la logique de Gödel vérifie la propriété d'interpolation de Lyndon, question ouverte depuis longtemps.
- décidabilité par recherche de preuves : nous avons proposé une approche constructive via la suppression de redondances durant la recherche et la méthode, mécanisée dans Coq, produit une procédure de décision pour la logique de relevance implicationnelle.

VALIDATION PAR DES OUTILS DE RAISONNEMENT AUTOMATIQUE
- Le démonstrateur VINTE implantant des calculs pour la logique contre-factuelle V et ses extensions, qui est le premier démonstrateur pour ces logiques.
- Le démonstrateur iiProve, qui est le premier démonstrateur pour des logiques intermédiares, utilisant des séquents “imbriqués”.

La recherche continuera suivant les trois axes du projet, à partir des résultats déjà obtenus :

TRADUCTIONS ENTRE CALCULS INTERNES ET EXTERNES
Nous souhaitons étudier des traductions de calculs avec hyperséquents et séquents “imbriqués” dans des calculs de séquents : le but sera d'obtenir une nouvelle classification de ces logiques fondée sur des restrictions dans la traduction et inversement sur des résultats négatifs sur l'expressivité pour les calculs de séquents. De plus, nous souhaitons étudier des traductions entre calculs internes existants et le nouveau calcul avec labels pour les logiques modales non normales.

DE NOUVEAUX CALCULS INTERNES A PARTIR DE CALCULS EXISTANTS ET APPLICATIONS
Nous souhaitons étudier comment dériver des calculs internes pour les extensions modales et épistémiques des logiques BI et BBI, à partir des calculs externes et comment les utiliser pour étudier la décidabilité des ces fragments. De plus, nous souhaitons étudier comment obtenir des calculs internes à partir des calculs “display” pour des logiques intermédiaires et sous-structurelles en considérant la forme invariante par résiduation de ces calculs.

VALIDATION PAR OUTILS DE RAISONNEMENT AUTOMATIQUE
Nous souhaitons implanter un démonstrateur fondé sur le calcul des tableaux pour les logiques BI et BBI, avec génération de contre-modèles. De même pour nos calculs avec labels pour les logiques modales non normales, ce qui en fera le premier démonstrateur pour ces logiques. Enfin nous souhaitons développer une traduction automatique entre les calculs internes et externes pour les logiques conditionnelles de Lewis.

Liste Partielle :
M. Girlando, B. Lellmann, N. Olivetti, and G.L. Pozzato. Hypersequent Calculi for Lewis Conditional Logics with Uniformity and Reflexivity. Proc. TABLEAUX 2017.

M. Girlando, B. Lellmann, N. Olivetti, G.L. Pozzato, and Q. Vitalis. VINTE: an Implementation of Internal Calculi for Lewis Logics of Counterfactual Reasoning. Proc. TABLEAUX 2017.

A. Ciabattoni and F. Genco. Hypersequents and Systems of Rules: Embeddings and Applications. ACM Transaction on Computational Logic 19(2), Article 11 (2018).

J-R. Courtault and H. van Ditmarsch and D. Galmiche. A Public Announcement Separation Logic. Proc. MSCS, 2017.

A. Ciabattoni, T. Lyon, and R. Ramanayake. From Display to Labelled Proofs for Tense Logics. Proc. LFCS 2018.

A. Ciabattoni and R. Ramanayake. Bunched Hypersequent Calculi for Distributive Substructural Logics. Proc. LPAR 2017.

T. Dalmonte, N. Olivetti, and S. Negri. Non-normal modal logics: bi-neighbourhood semantics and its labelled calculi. Proc. AIML 2018.

D. Galmiche and M. Marti and D. Méry. Proof Translations in BI Logic -extended abstract. 1st Int. Workshop EICNCL 2018, Oxford, UK, July 2018.

D. Galmiche and D.Méry. Labelled Connection-based Proof Search for Multiplicative Intuitionistic Linear Logic. 3rd Int. Workshop ARQNL 2018, Oxford, UK, July 2018.

M. Girlando, S. Negri, and N. Olivetti. Counterfactual logic: labelled and internal calculi, two sides of the same coin? Proceedings AIML 2018.

R. Kuznets and B. Lellmann. Interpolation for Intermediate Logics via Hyper- and Linear Nested Sequents. Proc. of AIML 2018.

D. Larchey-Wendling. Constructive Decision via Redundancy-free Proof-Search. Proc. IJCAR 2018.

M. Marti and Th. Studer. The internalized Disjunction Property for Intuitionistic Justification Logic. Proc. AIML 2018

L. Santocanale. The equational theory of the natural join and inner union is decidable. Proc. FOSSACS 2018.

L'utilisation fructueuse d'approches logiques dans de nombreux domaines des sciences de l'informatique, de l'épistémologie, et de l'intelligence artificielle, a conduit à une multiplication de nouveaux formalismes en logique même. Ces formalismes disposent d'un pouvoir expressif plus étendu que celui de la logique classique, autorisant du même coup une granularité plus fine dans l'analyse de notions qui ne s'expriment pas naturellement avec le langage de la logique classique. Ces formalismes permettent la représentation de différents modes de vérité d'une formule (logiques modales), ainsi que la représentation d'autres formes de raisonnement, de type hypothétique et plausible (logiques conditionnelles), sur la connaissance (logiques épistémiques), ou sur la séparation et le partage de ressources (logiques BI de « bunched implication »). Ces logiques permettent en outre de modéliser différents systèmes, et d'établir leur propriétés par l'intermédiaire de cadres de preuve assurant un comportement adéquat.
Dans ce projet nous considérons des logiques qui généralisent les logiques modales (incluant les formalismes évoqués) et qui sont caractérisés par des variantes des sémantiques de Kripke et dont le domaine d'application couvre la vérification formelle, l'épistémologie et la représentation des connaissances.
Nos recherches porteront sur les cadres de preuve de ces logiques. L'intérêt de la théorie de la preuve est qu'elle fournit, par la constitution d'un calcul analytique associé, une approche constructive pour l'étude des propriétés méta-logiques et calculatoires du système étudié. De plus, la notion de calcul analytique est au coeur du développement d'outils tels que démonstrateurs et assistants de preuve.
Dans la littérature des trente dernières années, de nombreux calculs, généralisant le calcul de séquents initialement proposé par Gentzen, ont été proposés pour les logiques modales et des systèmes associés (calculs hyperséquents, calculs étiquetés, "display calculi"). Les systèmes de preuve en question se partagent en deux catégories : d'une part les calculs internes au sein desquels tout objet élémentaire peut être interprété comme une formule du langage, d'autre part les calculs externes dont les objets élémentaires sont les formules d'un langage plus expressif encodant partiellement la sémantique. Les résultats obtenus sur l'ensemble de ces systèmes est mitigé : pour certaines classes importantes de logiques, aucun calcul interne n'est connu, tandis que pour d'autres classes, aucun calcul externe optimal, voire garantissant une terminaison, n'a été établi. Les deux types de calcul représentent pourtant des façons distinctes d'aborder la logique, toutes deux utiles et complémentaires. Les relations entre calculs internes et externes est un sujet très peu exploré.
Notre objectif principal se rapporte à une étude systématique des relations entre ces deux approches dans le but de féconder chacune d'elles avec les avantages respectifs de l'autre. Une telle étude doit jeter une lumière nouvelle sur la notion de prouvabilité tant du coté des calculs syntaxiques que du coté des calculs sémantiques, permettre le transfert de propriétés d'un calcul à l'autre, et conduire à la découverte de calculs internes pour les logiques qui n'en sont pas dotées. Enfin, la découverte de nouveaux calculs internes permettra d'aborder des problèmes théoriques encore ouverts autour de la conservativité, l'interpolation, et la décidabilité.
En résumé, le projet TICAMORE, en clarifiant la relation liant deux approches fondamentales, mais historiquement séparées, apportera une vision unificatrice permettant d'aborder des problèmes théoriques importants et toujours ouverts. Il contribuera en outre au développement de nouveaux outils automatiques de raisonnement.