Modalny jezyk zapytan MDatalog

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

$$\forall\overline{x}\ \Box^s (A \gets B_1, \ldots, B_k)$$

gdzie $s \geq 0$, $k \geq 0$, oraz

• A, B₁, ..., B_k sa formuami postaci $\Box \phi$, $\Diamond\phi$, lub $\phi$, gdzie $\phi$ jest klasycznym atomem;

• $\overline{x}$ sa wszystkimi zmiennymi wystepujacymi w $(A \gets B_1, \ldots, B_k)$;

• jezeli k=0, to regua nie zawiera zadnej zmiennej ani zadnego kwantyfikatora;

• wszystkie zmienne wystepujace w A wystepuja takze w $(B_1, \ldots, B_k)$.

Definicja Zapytaniem jest formua postaci $\exists\overline{x}\ \phi(\overline{x})$, gdzie $\phi$ jest pozytywna formua bez kwantyfikatorów a $\overline{x}$ jest wektorem (mozliwie pustym) wszystkich zmiennych wystepujacych w $\phi$.

Ustalmy normalna logike pierwszego rzedu L. Dla danego programu P w jezyku MDatalog i danego zapytania $\exists\overline{x}\ \phi(\overline{x})$, chcemy sprawdzic czy $P \models_L \exists\overline{x}\ \phi(\overline{x})$ i znalezc wszystkie wektory symboli staych $\overline{c}$ takie, ze $P \models_L \phi(\overline{c})$.

Modele Kripkego pierwszego rzedu moga byc uporzadkowane w sposób podobny jak dla wersji zdaniowej.

Definicja Niech $M = \langle D, W, \tau, R, m \rangle$ i $N = \langle {{D}'}, {{W}'}, {{\tau}'}, {{R}'}, {{m}'} \rangle$ beda modelami Kripkego pierwszego rzedu. Mówimy, ze M jest mniejszy lub równy N wzgledem funkcji $f : D \to {{D}'}$ i relacji binarnej $r \subseteq W \times {{W}'}$ jezeli

1.

$r(\tau ,{{\tau}'})$

2.

$\forall x,{{x}'},y\;\ R(x,y) \land r(x,{{x}'}) \to \exists{{y}'}\ {{R}'}({{x}'},{{y}'}) \land r(y,{{y}'})$

3.

$\forall x,{{x}'},{{y}'}\;\ {{R}'}({{x}'},{{y}'}) \land r(x,{{x}'}) \to \exists y\ R(x,y) \land r(y,{{y}'})$

4.

Dla dowolnego symbolu staego c_i, f(c_i^M) = c_i^N.

5.

Dla dowolnych $x \in W$ i ${{x}'} \in {{W}'}$ takich, ze r(x,x'), dla dowolnego symbolu relacyjnego R_j arnosci n i elementów a₁, ..., a_n dziedziny D, jezeli ${R_j}^{M,x}(a_1, \ldots, a_n)$, to ${R_j}^{N,{{x}'}}(f(a_1), \ldots, f(a_n))$.

Mówimy, ze M jest mniejszy lub równy N, i piszemy $M \leq N$, jezeli M jest mniejszy lub równy N wzg. pewnej f i pewnej r.

W pracy pokazaem, ze relacja $\leq$ miedzy modelami Kripkego pierwszego rzedu jest porzadkiem czesciowym. Ponadto, jezeli $M \leq N$, to dla dowolnej pozytywnej formuy $\phi$ bez zmiennych i kwantyfikatorów, jezeli $M \vDash\phi$, to $N \vDash\phi$.

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.