Herbrand-Expansion

Die Herbrand-Expansion stellt eine Menge von Prädikaten (siehe Prädikatenlogik dar, mittels derer die Unerfüllbarkeit einer prädikatenlogischen Formel in einer aussagenlogischen Form abgebildet werden kann. Die Herbrand-Expansion wurde nach dem französischen Logiker Herbrand benannt.

Definition

Sei $F=\forall y_{1}\forall y_{2}...\forall y_{n}F^{*}$ eine geschlossene Formel in Skolemform, F* bezeichne die 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) substituiert, alle Möglichkeiten werden durchgespielt.