Arithmétique de Presburger
Pour les articles homonymes, voir Pressburger.
En logique mathématique, l'arithmétique de Presburger est la théorie du premier ordre des nombres entiers naturels munis de l'addition. Elle a été introduite en 1929 par Mojżesz Presburger. Il s'agit de l'arithmétique de Peano sans la multiplication, c’est-à-dire avec seulement l'addition, en plus du zéro et de l'opération successeur. Contrairement à l'arithmétique de Peano, l'arithmétique de Presburger est décidable. Cela signifie qu'il existe un algorithme qui détermine si un énoncé du langage de l'arithmétique de Presburger est démontrable à partir des axiomes de l'arithmétique de Presburger.
Définition
modifierLa signature du langage de l'arithmétique de Presburger contient les symboles de constantes 0 et 1, le symbole de fonction binaire +. L'arithmétique est définie par les axiomes suivants :
- ∀x, ¬(0 = x + 1)
- ∀x,∀y, x + 1 = y + 1 → x = y
- ∀x, x + 0 = x
- ∀x, ∀y, x + (y + 1) = (x + y) + 1
- Pour toute formule P(x, y1, …, yn) du premier-ordre sur le langage de l'arithmétique de Presburger avec x, y1, …, yn comme variables libres, la formule suivante est un axiome : ∀y1…∀yn [(P(0, y1, …, yn) ∧ ∀x(P(x, y1, …, yn) → P(x + 1, y1, …, yn))) → ∀y P(y, y1, …, yn)].
(5) est le schéma d'induction et c'est un ensemble infini d'axiomes. On peut montrer que l'arithmétique de Presburger n'est pas finiment axiomatisable en logique du premier ordre.
Propriétés
modifierMojżesz Presburger a démontré en 1929 que son arithmétique, qui est cohérente[1], est complète[2],[3]. Comme une théorie axiomatique récursivement axiomatisable et complète est décidable, on en déduit l'existence d'un algorithme qui décide, étant donné une proposition du langage de l'arithmétique de Presburger, si celle-ci est démontrable ou non.
Contrairement à l'arithmétique de Presburger, l'arithmétique de Peano n'est pas complète en vertu du théorème d'incomplétude de Gödel. L'arithmétique de Peano n'est pas décidable (voir problème de la décision).
Algorithmes
modifierConsidérons ici le problème de décision suivant : décider si une formule de l'arithmétique de Presburger est vraie. En 1974, Michael J. Fisher et Michael O. Rabin ont démontré que ce problème de décision a une complexité temporelle intrinsèque doublement exponentielle[4]. En d'autres termes, le problème de décision est 2EXPTIME-dur : il fait partie des problèmes les plus difficiles de la classe de complexité 2EXPTIME, qui est la classe des problèmes décidables en temps doublement exponentiel.
Il existe une procédure de décision non élémentaire reposant sur la théorie des automates finis[5].
Oppen en 1978 a donné un algorithme triplement exponentiel[6], c'est-à-dire que le problème de savoir si une formule de l'arithmétique de Presburger est vraie est dans 3EXPTIME, la classe des problèmes décidables en temps triplement exponentiel.
Berman en 1980 a donné un résultat plus précis de théorie de la complexité en utilisant des machines alternantes[7] : l'arithmétique de Presburger est complète pour la classe des problèmes décidés en temps 22nO(1) et n alternations, où le nombre n est la taille de la formule à vérifier. Cette classe contient 2EXPTIME et est contenu dans 3EXPTIME.
Le solveur SMT Z3 implémente l'arithmétique de Presburger[réf. nécessaire]. L'assistant de preuve Coq fournit la stratégie omega[réf. nécessaire].
Comparaison avec d'autres arithmétiques
modifierL'arithmétique de Peano est définie sur le langage de l'arithmétique de Presburger avec en plus un symbole de fonction binaire × dont l'interprétation intuitive est la multiplication. L'arithmétique de Peano contient des axiomes supplémentaires. L'arithmétique de Robinson, elle, ne contient pas le schéma d'induction.
Notes et références
modifier- On ne peut démontrer l'absurde, ou encore il existe un modèle, en fait le modèle standard des entiers naturels.
- Toute proposition est démontrable ou sa négation est démontrable.
- David, Nour, Raffali, Introduction à la logique, théorie de la démonstration, Dunod, (2003), p.136
- Michael Jo Fischer et Michael O. Rabin, « Super-Exponential Complexity of Presburger Arithmetic », dans Complexity of Computation: Proceedings of a Symposium in Applied Mathematics of the American Mathematical Society and the Society for Industrial and Applied Mathematics, , 27–41 p. (lire en ligne).
- Olivier Carton, Langages Formels, Calculabilité Et Complexité, Vuibert, , 236 p.
- Derek C. Oppen, « A 2^2^2^pn upper bound on the complexity of Presburger Arithmetic », Journal of Computer and System Sciences, vol. 16, , p. 323–332 (DOI 10.1016/0022-0000(78)90021-1, lire en ligne, consulté le )
- Leonard Berman, « The complexity of logical theories », Theoretical Computer Science, vol. 11, , p. 71–77 (DOI 10.1016/0304-3975(80)90037-7, lire en ligne, consulté le )
