Nerekurzivní DATALOG

• Tv.: Vyhodnocený program poskytuje pro každý predikát z IDB množinu tvrzení, která tvoří

• 1. množinu právě těch tvrzení, dokazatelných

• z EDB aplikací pravidel z IDB.

• 2. pro EDB + IDB minimální model.

• Důkaz: indukcí na pořadí pravidel.