Stratification (mathematics)

rdf:langString Stratifikation (Logik)

rdf:langString 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 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 positiv abhängig von einem Prädikat , kommt also im Kopf einer Regel vor, in der positiv im Rumpf vorkommt, dann muss eine größere oder die gleiche Stratifikationsnummer besitzen wie , also (B) Wenn ein Prädikat von einem negierten Prädikat abhängt, also im Kopf einer Regel vorkommt, in der negativ im Rumpf vorkommt, dann muss die Stratifikationsnummer von echt größer als die von sein, also 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 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). ist eine mögliche Stratifikation dieses Programms.