Blog personnel d'Arthur Milchior

-Si vous vous intéresser aux résultats présenté dans cette thèse (énoncé ci-dessous), sachez que je serai prêt aussi prêt à vous présenter ces résultats n'importe quand (par exemple au séminaire automate du 17 juin, où j'ai un quart d'heure de plus et où je peux me concentrer sur un résultat)
-Où alors, et ça concernera probablement plus de monde, vous pensez que vous ne comprendrez rien à ce dont la thèse peut parler. Si ça vous amuse de voir à quoi ressemble une soutenance de thèse, que vous pensez que c'est important de venir, etc... n'hésitez pas à venir. Mais si comme moi, quand on vous parle de recherche (et que ce n'est pas votre domaine), vous avez surtout l'impression d'entendre des gens parler une langue étrangère, que seul quelques inconnus au premier rang sont capable de distinguer d'un discours de médecin de molière, alors n'hésitez surtout pas à ne pas venir. Ou alors venez au pot, qui devrait être approximativement vers 16 heures. (Ami-e-s vegan, il y aura des gâteaux pour vous, et je m’assurerai de les marquer comme tels)

Ce manuscrit traite de la logique du premier ordre avec la relation d'ordre et les prédicats modulaires, notée FO<,mod. La classe des ensembles réguliers, c'est à dire des ensembles FO<,mod-définissables, est la classe des ensembles acceptés par un automate en base 1. C'est aussi la plus grande classe C d'ensembles telle que FOC ne définisse que des langages réguliers. Il est donc naturel de s'intéresser à cette logique et nous donnons dans ce manuscrit de nouvelles caractérisations des ensembles réguliers. Nous montrons que les ensembles réguliers ont une caractérisation en terme d'ensembles de dimension inférieure et en terme de périodicité. Nous montrons que si un ensemble R est définissable dans l'arithmétique de Presburger, alors il est régulier si et seulement si toutes les fonctions unaires FO<,R-définissable sont réguliers. Cette caractérisation nous sert à montrer que le fragment maximal C de l'arithmétique de Presburger tel que la satisfiabilité de FO<,C soit décidable est la classe des ensembles réguliers. Similairement, la satisfiabilité de la logique du premier ordre sur les mots avec la fonction successeur et une fonction unaire f croissante est indécidable dès que n-f(n) est non borné. Si f est non interprété, la logique du premier ordre avec la fonction successeur et f est indécidable sur les entiers. Enfin, on donne un algorithme en temps linéaire prenant en entrée un automate A en base b supérieur à 1 et acceptant si et seulement si A accepte un ensemble régulier. Un deuxième algorithme, en temps quasi-cubique, retourne alors une FO<,mod-formule qui définit l'ensemble d'entiers accepté par l'automate.

P.S: pour rappel, il y a deux ans j'écrivais ça sur la soutenance de thèse.