## [Herbrand-Basis](/de/node/60824) 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.