Herbrand-Expansion

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 $F=\mathrm{\forall }{y}_1\mathrm{\forall }{y}_2...\mathrm{\forall }{y}_n{F}^{*}$ eine geschlossene Formel in Skolemform, F* bezeichne die quantorenfreie Matrix.

Für F wird die Herbrand-Expansion E(F) definiert mit:

$E\left(F\right)=\{F^{*}[y_1/t_1][y_2/t_2]...[y_n/t_n]|t_1...t_n\in D\left(F\right)\}$

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 $F=\mathrm{\forall }x\mathrm{\forall }y\mathrm{\forall }zP(x,f(y),g(z,x))$

Dann ist $D\left(F\right)=\{a,f(a),g(a,a),f(g(a,a)),g(f(a),f(a)),...\}$, siehe Herbrand-Universum.

Die einfachsten Formeln in $E\left(F\right)$ sind:

$P(a,f(a),g(a,a))$	mit	$[x/a][y/a][z/a]$
$P(f(a),f(a),g(a,f(a)))$	mit	$[x/f(a)][y/a][z/a]$
$P(a,f(a),g(g(a,a),a))$	mit	$[x/a][y/a][z/g(a,a)]$

Man beachte, dass in diesem Fall $E\left(F\right)$ 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.