LOGIPEDIA — LOGIPEDIA:

Logipedia est une encyclopédie de démonstrations formelles universelle et en ligne. Nous avons le projet de soumettre une proposition au European call INFRAIA-02-2020: Integrating activities for starting communities, le 17 mars 2020, pour la développer et la transformer en une e-infrastructure européenne. Notre projet à long terme est de construire, en vingt ans, une encyclopédie qui contienne toutes les démonstrations formelles développées. Les démonstrations formelles et les méthodes formelles sont aujourd'hui une composante essentielle de certains projets industriels avancés. Par exemple, la maîtrise des méthodes formelles est un élément clé pour donner à l'Europe un avantage compétitif sur le marché des véhicules autonomes. Elles sont aussi un aspect important de l'évolution des mathématiques, car elles permettent de construire des démonstrations beaucoup plus complexes. Mais l'absence de standard limite cet impact, car elle limite les possibilité d'interaction entre les systèmes de démonstrations et la durabilité de ces démonstrations. Cela constitue la principale motivation de notre projet d'encyclopédie de démonstrations formelles universelle et en ligne. Une première étape dans cette direction a été le colloque de lancement de Logipedia qui a rassemblé 38 chercheurs autrichiens, tchèques, français, italiens, néerlandais et polonais. Depuis, des collègues belges, allemands, serbes, suédois et britanniques ont rejoint le projet. Une telle encyclopédie a nécessairement une ambition mondiale, mais, comme plusieurs systèmes de démonstrations développés dans le monde sont européens, l'Europe peut y jouer un rôle majeur, sans bien entendu exclure nos collègues extra-européens. La conception d'une telle encyclopédie réponds à plusieurs objectifs : rendre les systèmes de démonstrations interopérables, rendre les démonstrations durables, restaurer l'universalité de la vérité logique et surtout rendre les démonstrations formelles accessibles aux non spécialistes : mathématiciens, ingénieurs et étudiants. Le développement d'une telle encyclopédie pose de nouvelles questions de recherche concernant l'expression de théories mathématiques dans un cadre logique commun, tel Dedukti, sur lequel Logipedia est fondée, l'analyse de démonstrations formelles pour déterminer dans quelles théories elles peuvent être exprimées et l'organisation de grand corpus de démonstrations, en particulier l'alignement de concepts, c'est-à-dire l'identification de structures isomorphes, tels les réels de Cauchy et de Dedekind. Notre consortium rassemble des équipes qui apportent une compétence dans le développement de systèmes de démonstrations, l'interopérabilité entre systèmes, l'utilisation de cadres logiques et le développement de grandes bibliothèques de démonstrations. Notre projet pour les années à venir se décline en plusieurs axes : - Définir en Dedukti les théories des systèmes Agda, Coq, Lean, PVS, Isabelle / HOL, HOL 4, Mizar, TLA+, et B, poursuivant le travail déjà effectué sur celles de Matita, HOL Light et FoCaLiZe. - Importer des bibliothèques dans Logipedia: des bibliothèques telles celles de Coq, Isabelle / HOL, HOL Light, Agda, etc., et des bibliothèques avancées telles MathComp, Mizar, Isabelle Archive of Formal Proofs, GeoCoq, Flyspeck, NASA PVS, etc. et des bibliothèques de démonstrations de correction de programme telles seL4, CompCert, etc. - Construire des outils pour analyser ces démonstrations et aligner les concepts. - Construire des outils pour indexer et parcourir cette encyclopédie. Ce projet répond à plusieurs des objectifs du European call INFRAIA-02-2020: Integrating activities for starting communities : la synergie, les données de recherche ouvertes, un accès plus large et plus efficace, l'éducation, les interaction plus étroites entre les chercheurs, la meilleure gestion d'un flux de données, l'innovation. Il répond aussi clairement à une activité transverse mentionnée : la science ouverte.