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.