– INFER

Ce projet réunit trois équipes par leur intérêt commun pour une nouvelle approche de la théorie de la démonstration, « l'inférence profonde », qui a été développée durant les cinq dernières années par un groupe de chercheurs réunis autour d'Alessio Guglielmi. Nous visons à raffiner son énorme potentiel et à l'appliquer à des problèmes liés aux fondements de la logique, ainsi qu'à des questions plus pratiques d'algorithmique des sytèmes de déduction. Parmis les problèmes théoriques il y a le besoin fondamental d'une théorie de l'identification correcte des démonstrations et son corollaire, l'obtention d'une approche vraiment générale des réseaux de démonstration. Une autre question très voisine est l'extension de l'interprétation de Curry-Howard à ces nouvelles représentations. Parmi les problèmes pratiques nous aborderons des questions de stratégie et de complexité en recherche des preuves, en particulier dans des systèmes d'ordre supérieur. Ces questions sont reliées intimement à la formulation même de ces logiques, et le rapport évident entre l'inférence profonde et des techniques bien établies---comme la déduction modulo et l'unification sur les quantificateurs---sont des sujets que nous avons l'intention d'approfondir, étant donné leur ancrage commun dans la théorie de la réécriture. Nous voulons aussi explorer la formulation et l'utilisation de systèmes logiques plus « exotiques », de nature non-commutative, dont l'intérêt provient de l'existence d'applications, comme en liguistique et en calcul quantique. Ceci prolonge naturellement certains des premiers travaux en inférence profonde. Il est assez évident que des résulats probants pourront obtenus pour les problèmes de la partie « pratique » de ce programme de recherche. La partie « théorique » par contre s'inscrit dans une quête qui avance pas à pas depuis des décennies maintenant, et il est difficile de faire des prédictions exacte, sauf que nous avons la certitude que notre positionnement autour de l'inférence profonde nous permettra des progrès substantiels.