Biographie

Logique

• Prouveurs en ligne: Pour se familiariser avec la déduction naturelle, les logiques modales (en particulier S4 et GL, la logique de Gödel-Lob), la méthode de preuve par résolution en logique de premier ordre, j'ai écrit des prouveurs en ligne, avec des styles très divers, méthode des tableaux, calcul des séquents, preuve par résolution.
• Livre : Messieurs Pascal Lafourcade , Stéphane Devismes , et moi-même, nous avons écrit un livre pour enseigner la logique aux étudiants de la licence de sciences : Logique et démonstration automatique
• Semantiques : Voici deux papiers dédiés à la sémantique de la logique intuitioniste propositionelle
  • Bijection entre les préordres sur un ensemble et les topologies d'Alexandroff sur cet ensemble.
  • Deux sémantiques de la logique intuitioniste de Tarski et de Kripke.
• Model Elimination : en démonstration automatique, la méthode, appelée en anglais Model Elimination, est une méthode pour construire des preuves en logique du premier ordre initialement présentée par D.W.Loveland. Cette méthode a été, depuis 1967, date de sa création, très utilisée mais mal expliquée. Dans le document comprendre la Model Elimination, que vous pouvez lire aussi dans sa version anglaise, je m'efforce de donner cette explication, en prouvant la correction et la complétude de la méthode, grâce à une séparation claire des cas propositionnel et du premier ordre et, dans le cas propositionnel, en montrant pourquoi les lemmes produits sont corrects.
• Alpha-Equivalence : en mathématiques, on a besoin de calculer l'égalité de deux expressions à un changement près des variables liées. Dans le cas le plus simple des lambda-expressions, nous montrons comment calculer avec ce texte court cette égalité sans utiliser les indices de De Bruijn

Maths

• Dans le cadre de mon étude de la relativité générale, j'ai essayé de comprendre ce qu'est un tenseur. Très déçu par les livres ou les sites internet sur ce sujet, j'ai tenté de préciser l'objet mathématique caché derrière ce mot. Voici ma présentation des tenseurs.
• J'étais très insatisfait de la présentation usuelle des dérivées partielles. Voici ma façon de corriger les notations et les usages des dérivées partielles
• J'étais fasciné par les suites de Goodstein. Ce sont des suites d'entiers qui prennent des valeurs énormes, mais dont Reuben Goostein a prouvé, en utilisant les ordinaux, qu'elles terminaient toujours avec la valeur 0. Il a été prouvé que l'arrêt de cette suite, ne pouvait pas être démontré dans l'arithmétique de Peano. Voici une présentation de ces suites , avec un programme Ocaml pour les calculer et une preuve de l'arrêt avec hélas quelques lemmes admis.

Physique

Théorie des langages

Contact