Interprétation Herbrand - Herbrand interpretation
En logique mathématique , une interprétation de Herbrand est une interprétation dans laquelle toutes les constantes et symboles de fonction se voient attribuer des significations très simples. Plus précisément, chaque constante est interprétée comme elle-même et chaque symbole de fonction est interprété comme la fonction qui l'applique. L'interprétation définit également les symboles de prédicat comme désignant un sous-ensemble de la base de Herbrand pertinente , spécifiant effectivement quels atomes fondamentaux sont vrais dans l'interprétation. Cela permet aux symboles d'un ensemble de clauses d'être interprétés de manière purement syntaxique , séparée de toute instanciation réelle.
L'importance des interprétations de Herbrand est que, si une interprétation satisfait un ensemble donné de clauses S, alors il existe une interprétation de Herbrand qui les satisfait. De plus, le théorème de Herbrand stipule que si S est insatisfiable alors il existe un ensemble fini insatisfiable d'instances fondamentales de l' univers Herbrand défini par S . Cet ensemble étant fini, son insatisfiabilité peut être vérifiée en temps fini. Cependant, il peut y avoir un nombre infini de tels ensembles à vérifier.
Il porte le nom de Jacques Herbrand .
Voir également
Remarques
 |
Cet article lié à la logique mathématique est un bout . Vous pouvez aider Wikipedia en l' étendant . |