2 mai 2011
Antoine Durand-Gasselin (LIAFA)L’arithmétique de Presburger (PA) est la théorie du premier ordre sur les entiers avec l’addition et la comparaison, sa décidabilité fut prouvée par Presburger au moyen d’une méthode d’élimination des quantificateurs. Une version raffinée de cette méthode a été montrée 3EXPTIME, une méthode donc efficace pour décider ce problème montré 2EXPSPACE hard. Nous avons préféré l’approche de Büchi, avec des automates: en représentant les vecteurs d’entiers par des mots, il donne une construction de l’automate acceptant les représentations des vecteurs solutions d’une formule. La force de cette approche, c’est l’obtention d’une représentation canonique pour chaque formule de l’arithmétique de Presburger. Je m’attacherai à présenter cette approche automatique pour l’arithmétique de Presburger) et à vous montrer les résultats que nous avons obtenus (résultat sur ces automates et complexité de leur construction inductive).