Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur Graph Search.
Concept
Arithmétique de Presburger
Résumé
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.
La 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.
Mojżesz Presburger a démontré en 1929 que son arithmétique, qui est cohérente, est complète. 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).
Considérons ici le problème de décision suivant : décider si une formule de l'arithmétique de Presburger est vraie. Michael J. Fisher et Michael O.
Source officielle
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.
Proximité ontologique