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
Definitionquery is a formula of the form
,
where
is a positive formula without quantifiers, and
is a vector of all variables occurring in
,
and can be empty.
Fix a first-order normal modal logic L. Given a MDatalog program P and a query
,
the goal is to check whether
,
and to find tuples of constant symbols
such that
.
First-order Kripke models can be ordered in a similar way as propositional Kripke models.
Definition
and
be first-order Kripke models. We say that M is less than or equal to N with respect to a function
and a binary relation
if
It is shown in the thesis that the relation
between first-order Kripke models is a pre-order, and that if M and N are first-order Kripke models and
,
then for every positive ground formula
,
if
then
.
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.