Développement : [Automate décidant l'arithmétique de Presburger : doublon]

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 :