Online-Bibliothek

Stratifikation (Mathematik)

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 Hornklauseln genau dann als stratifizierbar bezeichnet, wenn es eine Abbildung S von der Menge der Prädikate auf 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, 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, 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.