La collection de toutes les formules atomiques ground (sans variables) obtenues en appliquant des symboles de prédicat à des n-uplets de termes provenant de l'univers d'Herbrand d'un langage.

Principe

Associer chaque prédicat n-aire à tous les n-uplets de termes ground de l'univers d'Herbrand pour générer toutes les atomes ground possibles ; la base est purement syntaxique, déterminée par la signature et l'univers d'Herbrand.

Démonstration

Avec le prédicat p/1 et l'univers d'Herbrand {a, f(a)}, la base d'Herbrand contient p(a) et p(f(a)) ; pour q/2 et l'univers {a,b} on a q(a,a), q(a,b), q(b,a), q(b,b).

Mauvaise application

Prétendre que la base d'Herbrand énumère exactement les atomes vrais d'une théorie sans fixer d'interprétation ou de modèle ; confondre la base avec l'ensemble des conséquences ou avec les atomes vrais d'un modèle particulier.

Conséquence

Fournit le domaine pour définir des interprétations d'Herbrand (affectations de valeurs de vérité aux atomes ground) et pour transformer des clauses en formes propositionnelles utilisées en preuve automatique et en programmation logique.

Inversion

Au lieu de l'ensemble complet des atomes syntactiques, considérer un modèle d'Herbrand particulier qui sélectionne un sous-ensemble comme vrai ; l'inversion met en lumière le passage de possibles atomes à attributions de vérité effectives.

Limite

Ne comprend que les formules atomiques construites à partir des symboles de prédicat du langage appliqués aux termes de l'univers d'Herbrand ; exclut les formules non atomiques, les variables, les constructions méta et les évaluations de vérité sans interprétation fixée.

Tension sémantique

Tension entre la base d'Herbrand comme réserve syntaxique de tous les atomes ground possibles et la notion sémantique de quels atomes sont vrais dans un modèle ; la base ne détermine pas la vérité par elle-même.

Synthèse

La base d'Herbrand est le catalogue syntaxique complet des atomes ground générables par les prédicats et l'univers d'Herbrand d'un langage ; elle sert de support aux interprétations d'Herbrand, à la mise à plat (grounding) et à la recherche de modèles.