Stratifikation (Logik)

Vorlage:Hinweisbaustein 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 <math>Q_1 \wedge \dots \wedge Q_n \wedge \neg Q_{n+1} \wedge \dots \wedge \neg Q_{n+m} \rightarrow P</math> 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 <math>P</math> positiv abhängig von einem Prädikat <math>Q</math>, kommt also <math>P</math> im Kopf einer Regel vor, in der <math>Q</math> positiv im Rumpf vorkommt, dann muss <math>P</math> eine größere oder die gleiche Stratifikationsnummer besitzen wie <math>Q</math>, also <math>S(P) \geq S(Q)</math>

(B) Wenn ein Prädikat <math>P</math> von einem negierten Prädikat <math>Q</math> abhängt, also <math>P</math> im Kopf einer Regel vorkommt, in der <math>Q</math> negativ im Rumpf vorkommt, dann muss die Stratifikationsnummer von <math>P</math> echt größer als die von <math>Q</math> sein, also <math>S(P) > S(Q)</math>

Horn-Klauseln sind stets stratifizierbar, da sie keine negativen Literale in den Körpern von Klauseln zulassen und daher nur Bedingung (A) zu erfüllen ist, was die triviale Abbildung <math>S</math> leistet, die allen Prädikatssymbolen dieselbe natürliche Zahl zuordnet.

Als Beispiel sei das folgende Prologprogramm gegeben:

<syntaxhighlight lang="prolog"> p(X) :- q(X). q(X) :- not(r(X)), s(X,Z). </syntaxhighlight>

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