DS10 - Défi des autres savoirs

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

Résumé de soumission

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.

Coordinateur du projet

Monsieur Nicola Olivetti (Laboratoire des Sciences de l'Information et des Systèmes)

L'auteur de ce résumé est le coordinateur du projet, qui est responsable du contenu de ce résumé. L'ANR décline par conséquent toute responsabilité quant à son contenu.

Partenaire

LORIA Laboratoire Lorrain de recherche en informatique et ses applications
TU WIen Technische Universität Wien, Department of Formal Languages, Theory and Logic Group
LSIS Laboratoire des Sciences de l'Information et des Systèmes

Aide de l'ANR 308 909 euros
Début et durée du projet scientifique : janvier 2017 - 36 Mois

Liens utiles