Wydział MIM UW - Modalny jezyk zapytan MDatalog

Next: Metody Up: No Title Previous: Definicje dotyczace logik modalnych

Modalny jezyk zapytan MDatalog

Jezyk zapytan MDatalog jest zdefiniowany i zinterpretowany w logikach modalnych pierwszego rzedu z sta $\l$ a dziedzina nad sygnatura bez funkcji.

Definicja Programem w jezyku MDatalog jest skonczony zbiór regu $\l$ postaci

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

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

A, B₁, ..., B_k sa formu $\l$ ami 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 regu $\l$ a nie zawiera zadnej zmiennej ani zadnego kwantyfikatora;
wszystkie zmienne wystepujace w A wystepuja takze w $(B_1, \ldots, B_k)$ .

Definicja Zapytaniem jest formu $\l$ a postaci $\exists\overline{x}\ \phi(\overline{x})$ , gdzie $\phi$ jest pozytywna formu $\l$ a 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 sta $\l$ ych $\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 sta $\l$ ego 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 pokaza $\l$ em, ze relacja $\leq$ miedzy modelami Kripkego pierwszego rzedu jest porzadkiem czesciowym. Ponadto, jezeli $M \leq N$ , to dla dowolnej pozytywnej formu $\l$ y $\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.

Next: Metody Up: No Title Previous: Definicje dotyczace logik modalnych

Nguyen Anh Linh
2000-04-01