Stratifikation (Logik)

Dieser Artikel oder nachfolgende Abschnitt ist nicht hinreichend mit Belegen (beispielsweise Einzelnachweisen) ausgestattet. Angaben ohne ausreichenden Beleg könnten demnächst entfernt werden. Bitte hilf Wikipedia, indem du die Angaben recherchierst und gute Belege einfügst.

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 sei 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.