Stratifikation (Logik)

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)$

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 $S$ leistet, die allen Prädikatssymbolen dieselbe natürliche Zahl zuordnet.

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.