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 ${\displaystyle 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 ${\displaystyle P}$ positiv abhängig von einem Prädikat ${\displaystyle Q}$, kommt also ${\displaystyle P}$ im Kopf einer Regel vor, in der ${\displaystyle Q}$ positiv im Rumpf vorkommt, dann muss ${\displaystyle P}$ eine größere oder die gleiche Stratifikationsnummer besitzen wie ${\displaystyle Q}$, also ${\displaystyle S(P)\geq S(Q)}$

(B) Wenn ein Prädikat ${\displaystyle P}$ von einem negierten Prädikat ${\displaystyle Q}$ abhängt, also ${\displaystyle P}$ im Kopf einer Regel vorkommt, in der ${\displaystyle Q}$ negativ im Rumpf vorkommt, dann muss die Stratifikationsnummer von ${\displaystyle P}$ echt größer als die von ${\displaystyle Q}$ sein, also ${\displaystyle 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 ${\displaystyle S}$ leistet, die allen Prädikatssymbolen dieselbe natürliche Zahl zuordnet.

Als Beispiel s​ei das folgende Prologprogramm gegeben:

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

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