Herbrand-Expansion
# 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=\forall y_{1}\forall y_{2}...\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)=\left\{F^{*}\left[y_{1}/t_{1}\right]\left[y_{2}/t_{2}\right]...\left[y_{n}/t_{n}\right]|t_{1}...t_{n}\in D\left(F\right)\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=\forall x\forall y\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\left(a,f(a),g(a,a)\right)$ | mit | $\left[x/a\right]\left[y/a\right]\left[z/a\right]$ |
| - | - | - |
| $P\left(f(a),f(a),g(a,f(a))\right)$ | mit | $\left[x/f(a)\right]\left[y/a\right]\left[z/a\right]$ |
| $P\left(a,f(a),g(g(a,a),a)\right)$ | mit | $\left[x/a\right]\left[y/a\right]\left[z/g(a,a)\right]$ |

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.

