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 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.
![{\displaystyle 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\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/5c9ef88f5c17d87c418446968285373769fdde4d)
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 |
![{\displaystyle \left[x/a\right]\left[y/a\right]\left[z/a\right]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/20d6947446363c8d41e4c1f6ea8e1d53d9c92b83)
![{\displaystyle \left[x/f(a)\right]\left[y/a\right]\left[z/a\right]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a75359be94fa0f1defb18cf5069b8de22de9a7e2)
![{\displaystyle \left[x/a\right]\left[y/a\right]\left[z/g(a,a)\right]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/97c2a0198f3dbe28f73b809d968e22158dc911ae)
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.