Entscheidungsproblem

Extrait.

En logique mathématique, on appelle problème de la décision ou, sous son nom d’origine en allemand, Entscheidungsproblem, le fait de déterminer de façon mécanique (par un algorithme) si un énoncé est un théorème de la logique égalitaire du premier ordre, c’est-à-dire s’il se dérive dans un système de déduction sans autres axiomes que ceux de l’égalité (exemples : système à la Hilbert, calcul des séquents, déduction naturelle). De façon équivalente par le théorème de complétude, il s’agit finalement de savoir si un énoncé est universellement valide, c’est-à-dire vrai dans tous les modèles (de l’égalité).