Stratifikation (Mathematik)

aus Wikipedia, der freien Enzyklopädie
Wechseln zu: Navigation, Suche

Stratifikation bezeichnet in der mathematischen Logik eine Ordnung von Prädikatensymbolen, die garantiert, dass eine eindeutige formale Interpretation eines Logikprogramms existiert. Insbesondere wird eine Menge von Klauseln der Form genau dann als stratifizierbar bezeichnet, wenn es eine Abbildung S von der Menge der Prädikate in die natürlichen Zahlen gibt, die die folgenden Bedingungen erfüllt:

(A) Ist ein Prädikat P positiv abhängig von einem Prädikat Q, kommt also P im Kopf einer Regel vor, in der Q positiv im Rumpf vorkommt, dann muss P eine größere oder die gleiche Stratifikationsnummer besitzen wie Q, also
(B) Wenn ein Prädikat P von einem negierten Prädikat Q abhängt, also P im Kopf einer Regel vorkommt, in der Q negativ im Rumpf vorkommt, dann muss die Stratifikationsnummer von P echt größer als die von Q sein, also

Als Beispiel sei das folgende Prologprogramm gegeben:

p(X) :- q(X)
q(X) :- not(r(X)), s(X,Z)

ist eine mögliche Stratifikation dieses Programms.