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 <math>F=\forall y_1 \forall y_2 ... \forall y_n F^*</math> eine geschlossene Formel in Skolemform, F* bezeichne die quantorenfreie Matrix.
Für F wird die Herbrand-Expansion E(F) definiert mit:
- <math>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\}</math>
- 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 <math>F=\forall x \forall y \forall z P( x, f(y), g(z,x) )</math>
Dann ist <math>D\left( F \right) = \{a, f(a), g(a,a), f(g(a,a)), g(f(a),f(a)),... \}</math>, siehe Herbrand-Universum.
Die einfachsten Formeln in <math>E \left(F \right)</math> sind:
| <math>P\left (a, f(a), g(a,a)\right)</math> | mit | <math>\left[ x / a \right]\left[ y / a \right]\left[ z / a \right]</math> |
| <math>P\left (f(a), f(a), g(a,f(a))\right)</math> | mit | <math>\left[ x / f(a) \right]\left[ y / a \right]\left[ z / a \right]</math> |
| <math>P\left (a, f(a), g(g(a,a),a)\right)</math> | mit | <math>\left[ x / a \right]\left[ y / a \right]\left[ z / g(a,a) \right]</math> |
Man beachte, dass in diesem Fall <math>E\left (F \right)</math> unendlich ist. Die Formeln können jetzt wie aussagenlogische Formeln (Aussagenlogik) behandelt werden, da sie keine Variablen enthalten.
Siehe auch
Literatur
- Schöning, Uwe: Logik für Informatiker. 5. Auflage. Spektrum Akademischer Verlag, Berlin 2000, ISBN 3-8274-1005-3.