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 Klauseln der Form $Q_1 \wedge \dots \wedge Q_n \wedge \neg Q_{n+1} \wedge \dots \wedge \neg Q_{n+m} \rightarrow P$ 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 $S(P) \geq S(Q)$

(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 $S(P)\;\! > S(Q)$

Als Beispiel sei das folgende Prologprogramm gegeben:

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

$S = \{p \mapsto 2, q \mapsto 2, r \mapsto 1, s \mapsto 1\}$ ist eine mögliche Stratifikation dieses Programms.