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
is called a Horn formula
iff one of the following conditions holds:
Definitionpositive propositional modal logic program, sometimes just called a positive program, is a finite set of
rules of the following form:
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
.
Definition
and
be Kripke models. We say that M is less than or equal to N wrt. a binary relation
,
and write
wrt. r, if:
It is shown in the thesis that the relation
between Kripke models is a pre-order, and that if
,
then for every positive formula
,
if
then
.
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.