Herbrand-Expansion

aus Wikipedia, der freien Enzyklopädie
Zur Navigation springen Zur Suche springen

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.

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.

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.

  • Schöning, Uwe: Logik für Informatiker. 5. Auflage. Spektrum Akademischer Verlag, Berlin 2000, ISBN 3-8274-1005-3.