Stratifikovaný DATALOG

• Tv.: Program P je stratifikovatelný právě když jeho závislostní graf neobsahuje cyklus s negativní hranou.

• Důkaz:  Každá virtuální relace P má přiřazen index strata, ve kterém je definována. Tedy (P,Q) je pozitivní  index(P)  index(Q)

• (P,Q) je negativní  index(P) < index(Q)

• Kdyby existoval cyklus s negativní hranou, existoval by uzel X, kde index(X) < index(X), což je spor.

•  dekomponujeme závislostní graf na silně souvislé komponenty, provedeme kondenzaci grafu, která je acyklická, a přiřadíme topologické upořádání komponentám.