Definition
Die Sammlung aller ground-atomaren Formeln (Variabelfreie Atome), die durch Anwendung von Prädikatsymbolen auf Tupel von Termen aus dem Herbrand-Universum gebildet werden können.

Prinzip

Prinzip
Kombiniere jedes n-stellige Prädikat mit allen n-Tupeln grounder Terme aus dem Herbrand-Universum, um alle möglichen ground-Atome zu erzeugen; die Basis ist rein syntaktisch und durch Signatur und Herbrand-Universum festgelegt.

Demonstration

Demonstration
Bei Prädikat p/1 und Herbrand-Universum {a, f(a)} enthält die Herbrand-Basis p(a) und p(f(a)); mit q/2 und Universum {a,b} enthält sie q(a,a), q(a,b), q(b,a), q(b,b).

Fehlanwendung

Fehlanwendung
Anzunehmen, die Herbrand-Basis liste genau die wahren Atome einer Theorie auf, ohne eine Interpretation oder ein Modell festzulegen; die Basis mit den Konsequenzen der Theorie oder mit den in einem Modell wahren Atomen zu verwechseln.

Konsequenz

Konsequenz
Dient als Domäne zur Definition von Herbrand-Interpretationen (Zuweisung von Wahrheitswerten zu ground-Atomen) und zum Grounding von Klauseln in propositionale Form, wie es in automatischem Beweisen und Logikprogrammierung gebraucht wird.

Umkehrung

Umkehrung
Statt der kompletten syntaktischen Menge ground-Atome betrachtet man ein bestimmtes Herbrand-Modell, das eine Teilmenge als wahr auswählt; die Umkehrung hebt den Übergang von möglichen Atomen zu tatsächlichen Wahrheitszuweisungen hervor.

Abgrenzung

Abgrenzung
Enthält nur atomare Formeln, die aus den Prädikaten des Sprachvokabulars auf Herbrand-Termen gebildet werden; schließt nicht-atomare Formeln, Variablen, Meta-Konstrukte und Wahrheitszuweisungen ohne feste Interpretation aus.

Semantische Spannung

Semantische Spannung
Spannung zwischen der Herbrand-Basis als syntaktischem Vorrat aller möglichen ground-Atome und der semantischen Frage, welche dieser Atome in einem Modell wahr sind; die Basis determiniert Wahrheit nicht von selbst.

Synthese

Synthese
Die Herbrand-Basis ist das vollständige syntaktische Verzeichnis der ground-Atome, die aus den Prädikaten und dem Herbrand-Universum einer Sprache erzeugt werden können; sie bildet die Grundlage für Herbrand-Interpretationen, Grounding und Modellfindung.