|
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 
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\}](lexikon/Mathematik-Logik-Herbrand-Expansion-1.png)
- 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.
siehe auch:
|
Startseite 
Bookmark setzen
Sitemap
Impressum
Lexikon Eintrag Drucken
Dokument als PDF downloaden