The Modal Query Language MDatalog

The modal query language MDatalog is defined and interpreted in fixed-domain first-order modal logics over signatures without functions.

DefinitionMDatalog program is a finite set of rules of the form

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

where $s \geq 0$, $k \geq 0$, and

• A, B₁, ..., B_k are formulae of the forms $\Box \phi$, $\Diamond\phi$, $\phi$, with $\phi$ being a classical atom.
• $\overline{x}$ are all variables occurring in $(A \gets B_1, \ldots, B_k)$.
• If k=0 then the rule is a ground fact, i.e. there is no quantifiers prefixing the rule.
• All variables occurring in A also occur in $(B_1, \ldots, B_k)$.

Definitionquery is a formula of the form $\exists\overline{x}\ \phi(\overline{x})$, where $\phi$ is a positive formula without quantifiers, and $\overline{x}$ is a vector of all variables occurring in $\phi$, and can be empty.

Fix a first-order normal modal logic L. Given a MDatalog program P and a query $\exists\overline{x}\ \phi(\overline{x})$, the goal is to check whether $P \models_L \exists\overline{x}\ \phi(\overline{x})$, and to find tuples of constant symbols $\overline{c}$ such that $P \models_L \phi(\overline{c})$.

First-order Kripke models can be ordered in a similar way as propositional Kripke models.

Definition $M = \langle D, W, \tau, R, m \rangle$ and $N = \langle {{D}'}, {{W}'}, {{\tau}'}, {{R}'}, {{m}'} \rangle$ be first-order Kripke models. We say that M is less than or equal to N with respect to a function $f : D \to {{D}'}$ and a binary relation $r \subseteq W \times {{W}'}$ if

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.

For any constant symbol c_i, f(c_i^M) = c_i^N.

5.

For any $x \in W$ and ${{x}'} \in {{W}'}$ such that r(x,x'), for any n-ary relation symbol R_j and elements a₁, ..., a_n of D, if ${R_j}^{M,x}(a_1, \ldots, a_n)$ then ${R_j}^{N,{{x}'}}(f(a_1), \ldots, f(a_n))$.

We say that a model M is less then or equal to N, and write $M \leq N$, if M is less then or equal to N with respect to some f and some r.

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

Given a MDatalog program P in a first-order 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.