Die Herbrand-Expansion stellt eine Menge von prädikatenlogischen Formeln dar, die aus einer gegebenen Formel F durch eine spezielle Art der Substitution abgeleitet werden können. Mit Hilfe dieser Formelmenge kann die Unerfüllbarkeit einer prädikatenlogischen Formel in einer aussagenlogischen Form abgebildet werden. Die Herbrand-Expansion wurde nach dem französischen Logiker Jacques Herbrand benannt.
Definition
Sei eine geschlossene Formel in Skolemform, F* bezeichne die quantorenfreie Matrix.
Für F wird die Herbrand-Expansion E(F) definiert mit:
D(F) ist das Herbrand-Universum von F.
Umgangssprachlich: Alle Variablen in der Matrix F* werden durch Terme aus D(F) ersetzt, alle Möglichkeiten werden durchgespielt. Man spricht auch von der Menge der Instanzen der Formel F.
Beispiel Sei
Dann ist , siehe Herbrand-Universum.
Die einfachsten Formeln in sind:
mit mit mit
Man beachte, dass in diesem Fall unendlich ist. Die Formeln können jetzt wie aussagenlogische Formeln (Aussagenlogik) behandelt werden, da sie keine Variablen enthalten.
Siehe auch Satz von Herbrand
Literatur Schöning, Uwe: Logik für Informatiker. 5. Auflage. Spektrum Akademischer Verlag, Berlin 2000, ISBN 3-8274-1005-3.
Kategorie:Mathematische Logik