January 6, 2014
Arthur Milchior (LACL - UPEC)FO[N,+], la logique du premier ordre, sur les entiers naturels, utilisant uniquement la fonction + et l’égalité, est une logique très étudiée, appelée Logique de Presburger. Je m’intéresse à trouver des ressemblances et des différences entre cette logique et FO[N,<,mod], la logique du premier ordre sur les entiers naturels avec la relation d'ordre entre les variables et des prédicats modulaires du style “x=a mod b” si et seulement si a est congru à la variable x mod b. Je parlerai dans cet exposé des deux principaux sujets sur lesquels j'ai travaillé en deux ans, de stage puis de thèse: - Il existe plusieurs manières de caractériser les ensembles de vecteurs d'entiers, c'est à dire de sous-ensembles de N^d pour un entier d, définissables dans la logique de Presburger. Il s'agit des ensembles semilinéaires, mais aussi des ensembles rationnels quand on regarde (N^d,+) comme un monoïde. Il s'agit aussi des ensembles qui respectent la caractérisation de Muchnik, et aussi des ensembles E tels que tous les ensembles d'entiers définissables dans FO[N,+,E] soient ultimement périodiques, c'est le théorème de Michaux-Villemaire. J'expliquerai que la caractérisation de Muchnik peut être modifiée de manière à caractériser les ensembles définissables dans FO[N,<,mod]. Que le théorème de Michaux-Villemaire peut être modifié pourvu qu'on rajoute l'hypothèse que les ensembles considérés soient semilinéaires. Enfin, j'expliquerai que cette propriété permet de prouver que la satisfiabilité de la logique FO[N,<,E] pour n'importe quel prédicat E semilinéaire non définissable dans FO[N,<,mod] est indécidable sur les mots. - De plus, si un automate fini reconnaît un ensemble de vecteurs d'entiers, il est possible de décider en temps polynomial si cet ensemble est semilinéaire, c'est à dire s'il est dans FO[N,+]. J'expliquerai comment le problème est précisément défini, et qu'un algorithme fort différent permet de caractériser les automates acceptant un ensemble définissable dans FO[N,<,mod] ainsi que dans quelques logiques encore moins expressives.