Modalne formuy Horna i pozytywne programy w zdaniowych logikach modalnych

Formua jest w normalnej postaci negatywnej jezeli kazda wystepujaca w niej negacja poprzedza bezposrednio zmienna zdaniowa. Formua jest nazwana negatywna jezeli w równowaznej jej formule w normalnej postaci negatywnej kazda zmienna zdaniowa jest poprzedzona przez negacje. Formua jest pozytywna jezeli jej negacja jest negatywna formua.

Definicja Formua $\phi$ jest nazwana formua Horna jezeli przynajmniej jeden z nastepujacych warunków zachodzi:

• $\phi$ jest zmienna zdaniowa

• $\phi$ jest formua negatywna

• $\phi = \Box \psi$, lub $\phi = \Diamond\psi$, lub $\phi = \psi \land \zeta$, gdzie $\psi$ i $\zeta$ sa formuami Horna

• $\phi$ jest dyzjunkcja formuy negatywnej i formuy Horna.

Definicja Pozytywnym programem w zdaniowych logikach modalnych jest skonczony zbiór regu nastepujacej postaci:

$$\Box^s (B_1 \land \ldots \land B_k \to A)$$

gdzie $s \geq 0$, $k \geq 0$, a $A, B_1, \ldots, B_k$ sa atomami jednej z postaci p, $\Box p$, $\Diamond p$, gdzie p jest zmienna zdaniowa. Czesto piszemy reguy w postaci:

$$\Box^s (A \gets B_1, \ldots, B_k).$$

W pracy pokazaem, ze mozna sprowadzic kazdy zbiór formu Horna X do pewnego programu P razem z pozytywna formua Q taka, ze dla dowolnej normalnej logiki modalnej L, X jest L-spenialny wtw, gdy $P \models_L Q$.

Definicja Niech $M = \langle W,\tau,R,h\rangle$ i $N = \langle {{W}'},{{\tau}'},{{R}'},{{h}'}\rangle$ beda modelami Kripkego. Mówimy, ze M jest mniejszy lub równy N wzgledem relacji binarnej $r \subseteq W \times {{W}'}$, i piszemy $M \leq N$ wzg. r, jezeli:

1.

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

2.

  $\forall x,{{x}'}\;\; r(x,{{x}'}) \to (h(x) \subseteq{{h}'}({{x}'}))$

3.

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

4.

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

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

W pracy pokazaem, ze relacja $\leq$ miedzy modelami Kripkego jest czesciowym porzadkiem. Ponadto, jezeli $M \leq N$, to dla dowolnej pozytywnej formuy $\phi$, jezeli $M \vDash\phi$, to $N \vDash\phi$.

Dla danego pozytywnego programu P w logice modalnej L, mówimy, ze M jest najmniejszym L-modelem dla P jezeli M jest L-modelem dla P i jest równy lub mniejszy niz kazdy L-model dla P.