Quelques problèmes dans l'arithmétique de Presburger et l'arithmétique de Skolem.

Denis Lugiez
Université de Provence (U1) Marseille (FRANCE)
Friday, 4 March, 2005 (All day)
NO

L'étude des nombres est un des domaines les plus ancien des mathématiques et a suscité la curiosité des mathématiciens depuis les temps les plus reculés. Depuis les travaux des logiciens du siècle précédent on sait qu'il est vain de vouloir tout connaitre de l'arithmétique dans laquelle on autorise la multiplication et l'addition. Mais ces logiciens ont aussi montré rapidement que si on n'utilise que l'addition (arithmétique de Presburger) ou que la multiplication (arithmétique de Skolem) alors on obtient des théories décidables. Ensuite l'informatique est arrivée, et on s'est aperçu que ces théories logiques qui semblaient n'etre que des objets logiques intéressants mais uniquement théoriques étaient très utiles pour plusieurs applications de cette discipline, en particulier pour l'étude formelle de systèmes informatiques ou modelisés par des sytèmes informatiques, domaine en plein developpement actuellement. On ne compte plus les systèmes de preuve automatiques ou semi-automatiques qui utilisent une procédure de décision de l'arithmétique de Presburger (reposant sur l'élimination de quantificateur ou des méthodes d'automates en général).

Cela relance l'intéret sur l'étude de ces théories et alors que le domaine semblait bien connu, on s'aperçoit que certains problèmes méritent d'être repris et que des questions intéressantes restent encore sans réponse satisfaisante. Le premier sujet que j'aborderai dans cet exposé concerne les différentes représentations des solutions d'une formule de l'arithmétique de Presburger. Celles-ci peuvent etre représentées par la formule (après élimination des quantificateurs par exemple), mais ausi par un ensemble semi-linéaire ou encore par un automate qui reconnait les représentations binaires des tuples de solutions. Chaque formalisme a des avantages et des inconvénients selon les calculs qu'on veut effectuer, et il est donc intéressant de passer efficacement de l'un à l'autre (si cela est possible). Le formalisme automate permet de représenter plus d'ensembles et caractériser les automates qui correspondent à l'arithmétique de Presburger est un résultat difficile du à Semenov. Muchnik en donne une preuve accessible mais sa méthode reste encore inutilisable en pratique. Je rappelerai les résultats obtenus par Latour et Leroux pour le calcul d'une formule à partir d'un automate et je présenterai les résultats que j'ai obtenus pour passer d'un automate à la forme semilinéaire pour certains types d'ensembles et des résultats (ou questions) sur la complexité des représentations. Je terminerai en donnant quelques indications sur les résultats récents de Leroux pour le passage automate vers formules.

Ensuite je parlerai du parent pauvre, l'arithmétique de Skolem, en rappelant rapidement quelques résultats de base sur cette théorie et je montrerai comment elle peut être utilisée pour prouver des résultats de décidabilité sur une théorie de multi-ensembles équipée d'opération(s) de comptage.