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

Bearbeiten

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

Bearbeiten

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

Bearbeiten

Literatur

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