Stratifikovaný DATALOG

• Tv.: Vyhodnocovací algoritmus se zastaví a dá MPB soustavy datalogických rovnic.

• Důkaz: PB plyne indukcí podle úrovní

• Pz.: Stratifikovatelný program má obecně více stratifikací. Ty jsou ekvivalentní, tj. vyhodnocení vede ke stejnému MPB (Apt, 1986).

• Tv.: Nerekurzivní programy DATALOGu vyjadřují právě ty dotazy, které jsou vyjádřitelné monotónní podmnožinou AR.

• Pz.: pozitivní relační algebra ARP {, , [ ], }.