Développement : Automate décidant l'arithmétique de Presburger [doublon : ne pas utiliser dans vos couplage]

Détails/Enoncé :

voir : https://agreg-maths.fr/developpements/197

On construit un automate qui reconnaît les entiers vérifiant une formule de l'arithmétique de Presburger, puis on l'utilise pour démontrer que l'arithmétique de Presburger est décidable.

Versions :