Jezyk zapytan MDatalog jest zdefiniowany i zinterpretowany w logikach modalnych pierwszego rzedu z staa dziedzina nad sygnatura bez funkcji.
Definicja Programem w jezyku MDatalog jest skonczony zbiór regu
postaci
Definicja Zapytaniem jest formua postaci
,
gdzie
jest pozytywna formu
a bez kwantyfikatorów a
jest wektorem (mozliwie pustym) wszystkich zmiennych wystepujacych w
.
Ustalmy normalna logike pierwszego rzedu L. Dla danego programu P w jezyku MDatalog i danego zapytania
,
chcemy sprawdzic czy
i znalezc wszystkie wektory symboli sta
ych
takie, ze
.
Modele Kripkego pierwszego rzedu moga byc uporzadkowane w sposób podobny jak dla wersji zdaniowej.
Definicja Niech
i
beda modelami Kripkego pierwszego rzedu. Mówimy, ze M jest mniejszy lub równy N wzgledem funkcji
i relacji binarnej
jezeli
W pracy pokazaem, ze relacja
miedzy modelami Kripkego pierwszego rzedu jest porzadkiem czesciowym. Ponadto, jezeli
,
to dla dowolnej pozytywnej formu
y
bez zmiennych i kwantyfikatorów, jezeli
,
to
.
Dla danego programu P w jezyku MDatalog w normalnej logice modalnej pierwszego rzedu L, mówimy, ze M jest najmniejszym L-modelem dla P jezeli M jest L-modelem (pierwszego rzedu) dla P i jest równy lub mniejszy niz kazdy L-model (pierwszego rzedu) dla P.