Modal Horn Formulae and Positive Propositional Modal Logic Programs

A formula is in the negative normal form if each of its negations occurs immediately before a primitive proposition. A formula is called negative if in its negative normal form every primitive proposition is prefixed by negation. A formula is called non-negative if it is not negative, and positive if its negation is a negative formula.

Definitionformula $\phi$ is called a Horn formula iff one of the following conditions holds:

• $\phi$ is a primitive proposition
• $\phi$ is a negative formula
• $\phi = \Box \psi$, or $\phi = \Diamond\psi$, or $\phi = \psi \land \zeta$, where $\psi$ and $\zeta$ are Horn formulae
• $\phi$ is a disjunction of a negative formula and a Horn formula.

Definitionpositive propositional modal logic program, sometimes just called a positive program, is a finite set of rules of the following form:

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

where $s \geq 0$, $k \geq 0$ and $A, B_1, \ldots, B_k$ are atoms of one of the forms p, $\Box p$, $\Diamond p$, where p is a primitive proposition. We often write program rules in the form:

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

It is shown in the thesis that we can translate any set X of Horn formulae to a positive program P and a positive formula Q such that for any normal modal logic L, X is L-satisfiable iff $P \nvDash_L Q$.

Definition $M = \langle W,\tau,R,h\rangle$ and $N = \langle {{W}'},{{\tau}'},{{R}'},{{h}'}\rangle$ be Kripke models. We say that M is less than or equal to N wrt. a binary relation $r \subseteq W \times {{W}'}$, and write $M \leq N$ wrt. r, if:

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}'})$

We say that a model M is less than or equal to N, and write $M \leq N$, if $M \leq N$ wrt. some r.

It is shown in the thesis that the relation $\leq$ between Kripke models is a pre-order, and that if $M \leq N$, then for every positive formula $\phi$, if $M \vDash\phi$ then $N \vDash\phi$.

Given a positive program P in a normal modal logic L, we say that M is the least L-model of P if M is a L-model of P and M is less than or equal to every L-model of P.