# An Iterative Fixpoint Semantics for MKNF Hybrid Knowledge Bases with
Function Symbols

Marco Alberti Dipartimento di Matematica e Informatica, University of
FerraraDipartimento di Scienze Chimiche, Farmaceutiche ed Agrarie, University
of FerraraDipartimento di Matematica e Informatica, University of
FerraraDipartimento di Ingegneria, University of Ferrara Riccardo Zese
Dipartimento di Scienze Chimiche, Farmaceutiche ed Agrarie, University of
FerraraDipartimento di Matematica e Informatica, University of
FerraraDipartimento di Ingegneria, University of Ferrara Fabrizio Riguzzi
Dipartimento di Matematica e Informatica, University of FerraraDipartimento di
Ingegneria, University of Ferrara Evelina Lamma Dipartimento di Ingegneria,
University of Ferrara

###### Abstract

Hybrid Knowledge Bases based on Lifschitz’s logic of Minimal Knowledge with
Negation as Failure are a successful approach to combine the expressivity of
Description Logics and Logic Programming in a single language. Their syntax,
defined by Motik and Rosati, disallows function symbols. In order to define a
well-founded semantics for MKNF HKBs, Knorr et al. define a partition of the
modal atoms occurring in it, called the alternating fixpoint partition. In
this paper, we propose an iterated fixpoint semantics for HKBs with function
symbols. We prove that our semantics extends Knorr et al.’s, in that, for a
function-free HKBs, it coincides with its alternating fixpoint partition. The
proposed semantics lends itself well to a probabilistic extension with a
distribution semantic approach, which is the subject of future work.

##  1 Introduction

When modelling complex domains it is of foremost importance to choose the
logic that better fits with what must be represented. Therefore, many
languages have been defined, based on First Order Logic such as Logic
Programming (LP) or Description Logic (DL). These languages share many
similarities but, on the other hand, they differ in the domain closure
assumption they make: closed-world assumption for LP and open-world assumption
for DLs.

Since many domains, such as legal reasoning [2], require different closure
assumptions to coexist in the same model, combinations of LP and DL have been
proposed by several authors. One of the most effective approaches is called
Minimal Knowledge with Negation as Failure (MKNF) [8]. MKNF was then applied
to define hybrid knowledge bases (HKBs) [11], which are defined as the
combination of a logic program and a DL KB.

In the original HKB language, function symbols are not allowed. However, this
is a feature that is useful in many domains. Consider, for example, the
behaviour of a virus, which can mutate and spillover may happen due to each
mutation. To trace the evolution of a virus, it is necessary to identify the
sequence of spillover events starting from the initial version of the virus.
We can represent the spillover count by Peano numbers, by means of a function
symbol $s/1$ modelling that, e.g., $s(Y)$ represents the spillover event that
follows the spillover identified by $Y$, which may have happened after another
spillover, and so forth.

In this paper, we propose to extend the HKB syntax with function symbols, and
we present an iterated fixpoint semantics for HKBs with Function Symbols
(HKBFS). We prove that our semantics coincides with that of [6] and [9] in the
case of HKBs not including function symbols, and therefore can be considered
an extension of that semantics to the case with function symbols.

The proposed semantics will also serve as the basis for a further
(probabilistic) extension of the language, based on a distribution semantics
approach, which is the subject of an ongoing effort.

We provide the necessary background notions in Section 2. We define the syntax
and semantics of HKBFSs in Section 3. In Section 4, we prove that our
semantics extends Knorr et al’s. We conclude the paper in Section 5.

##  2 Background

In this section, we provide the necessary background notions on the syntax and
semantics of the language of MKNF Hybrid Knowledge Bases, which we extend with
function symbols in Section 3. We start with Description Logics, which are a
part of the language of HKBs.

###  2.1 Description Logics

Description Logics (DLs) are decidable fragments of First Order Logic used to
model ontologies [4]. Usually their syntax is based on concepts and roles,
corresponding to unary and binary predicates, respectively. In the following
we briefly recall the DL $\mathcal{ALC}$; see [3] for a complete introduction
to DLs.

$\mathcal{ALC}$’s alphabet is composed of a set $\mathbf{C}$ of _atomic
concepts_ , a set $\mathbf{R}$ of _atomic roles_ and a set $\mathbf{I}$ of
individuals. A _concept_ $C$ is defined by:

$\displaystyle C::=$ $\displaystyle C_{1}|\bot|\top|(C\sqcap C)|(C\sqcup
C)|\neg C|\exists R.C|\forall R.C$

where $C_{1}\in\mathbf{C}$ and $R\in\mathbf{R}$.

A _TBox_ ${\cal T}$ is a finite set of concept inclusion axioms $C\sqsubseteq
D$, where $C$ and $D$ are concepts. An _ABox_ ${\cal A}$ is a finite set of
concept membership axioms $a:C$ and role membership axioms $(a,b):R$, where
$C$ is a concept, $R\in\mathbf{R}$ and $a,b\in\mathbf{I}$. An $\mathcal{ALC}$
knowledge base ${\cal K}=({\cal T},{\cal A})$ consists of a TBox ${\cal T}$
and an ABox ${\cal A}$.

DL axioms can be mapped to FOL formulas by the transformation $\pi$ shown in
Table 1 for the $\mathcal{ALC}$ DL [16]. $\pi$ is applied to concepts as
follows:

$\begin{array}[]{rcl}\pi_{x}(A)&=&A(x)\\\ \pi_{x}(\neg C)&=&\neg\pi_{x}(C)\\\
\pi_{x}(C\sqcap D)&=&\pi_{x}(C)\wedge\pi_{x}(D)\\\ \pi_{x}(C\sqcup
D)&=&\pi_{x}(C)\wedge\pi_{x}(D)\\\ \pi_{x}(\exists R.C)&=&\exists
y.R(x,y)\wedge\pi_{y}(C)\\\ \pi_{x}(\forall R.C)&=&\forall
y.R(x,y)\rightarrow\pi_{y}(C)\\\ \end{array}$

Axiom | Translation
---|---
$C\sqsubseteq D$ | $\forall x.\pi_{x}(C)\rightarrow\pi_{x}(D)$
$a:C$ | $\pi_{a}(C)$
$(a,b):R$ | $R(a,b)$
$a=b$ | $a=b$
$a\neq b$ | $a\neq b$
Table 1: Translation of $\mathcal{ALC}$ axioms into FOL.

###  2.2 MKNF-based Hybrid Knowledge Bases

The logic of Minimal Knowledge with Negation as Failure (MKNF) was introduced
in [8] to support epistemic queries on logic programs. MKNF was inspired by
several works [7, 13] on epistemic query answering on non-monotonic databases,
which is essential when databases contain incomplete information.

The syntax of MKNF is the syntax of FOL augmented with the modal operators
$\mathbf{K}\,$ and $\mathbf{not}{\,}$.

MKNF-based Hybrid Knowledge Bases [11] are combinations of DL axioms and LP
rules that can be mapped to a MKNF formula, as follows. As shown in [11],
MKNF-based HKBs exhibits desirable properties (faithfulness, i.e.,
preservation of the semantics of both formalisms when the other is absent;
tightness, i.e., no layering of LP and DL; flexibility, i.e., the possibility
to view each predicate under both open and closed world assumption;
decidability), which each of the other existing approaches to LP and DL
integration lacks at least partly.

######  Definition 1.

A Hybrid Knowledge Base (HKB) is a pair
$\mathcal{K}=\langle\mathcal{O},\mathcal{P}{}\rangle$ where $\mathcal{O}$ is a
set of axioms in a description logic (Section 2.1) and $\mathcal{P}$ is a
finite set of normal function-free logic programming rules.

In the rest of the paper, with a slightly abuse of notation, we will say that
a HKB $\mathcal{K}_{1}=\langle\mathcal{O}_{1},\mathcal{P}{}_{1}\rangle$ is a
subset of a HKB
$\mathcal{K}_{2}=\langle\mathcal{O}_{2},\mathcal{P}{}_{2}\rangle$, i.e.,
$\mathcal{K}_{1}\subseteq\mathcal{K}_{2}$ iff
$\mathcal{O}_{1}\subseteq\mathcal{O}_{2}$ and
$\mathcal{P}{}_{1}\subseteq\mathcal{P}{}_{2}$. Given a HKB
$\mathcal{K}=\langle\mathcal{O},\mathcal{P}{}\rangle$, an atom in
$\mathcal{P}$ is a _DL-atom_ if its predicate occurs in $\mathcal{O}$, a non-
DL-atom otherwise.

######  Definition 2 (DL-safety).

A rule is _DL-safe_ if each of its variables occurs in at least one positive
non-DL-atom in the body; a HKB is _DL-safe_ if all its rules are DL-safe.

In this paper, we assume that all HKBs are DL-safe.

An HKB $\mathcal{K}=\langle\mathcal{O},\mathcal{P}{}\rangle$ can be mapped to
an MKNF formula by extending the standard transformation $\pi$ for DL axioms
(Table 1) to support LP rules:

  * •

if $r$ is a rule of the form $h\leftarrow
a_{1},\ldots,a_{n},\sim\\!\\!b_{1},\ldots,\sim\\!\\!b_{m}$ where all $a_{i}$
and $b_{j}$ are atoms and $\mathbf{X}$ is the tuple of all variables in $r$,
then
$\pi({r})=\forall\mathbf{X}(\mathbf{K}\,a_{1}\wedge\ldots\wedge\mathbf{K}\,a_{n}\wedge\mathbf{not}{\,}b_{1}\wedge\ldots\wedge\mathbf{not}{\,}b_{m}\rightarrow\mathbf{K}\,h)$

  * •

$\pi({\mathcal{P}})=\bigwedge_{r\in\mathcal{P}}\pi({r})$

  * •

$\pi({\langle\mathcal{O},\mathcal{P}{}\rangle})=\mathbf{K}\,\pi({\mathcal{O}})\wedge\pi({\mathcal{P}})$

This transformation is a way to give a semantics to a HKB: MKNF formulas have
been given two-valued [11] and three-valued [6] semantics, so the (two or
three-valued) semantics of the resulting MKNF formula can be taken as the
semantics of the original HKB. We refer the reader to those articles for an
in-depth discussion of the semantics and their respective merits.

In the following, we recall the three-valued MKNF semantics, which is more
relevant to our work. For simplicity, we omit the signature $\Sigma$ from the
definitions.

#### Three-valued MKNF semantics [6]

The truth of an MKNF formula $\psi$ is defined relatively to a _three-valued
MKNF structure_ $(I,\mathcal{M},\mathcal{N})$, which consists of a first-order
interpretation $I$ over a universe $\Delta$ and two pairs
$\mathcal{M}=(M,M_{1})$ and $\mathcal{N}=(N,N_{1})$ of sets of first-order
interpretations over $\Delta$ where $M_{1}\subseteq M$ and $N_{1}\subseteq N$.
$\mathbf{K}\,\psi$ is true (resp. false) with respect to $(M,M_{1})$ if and
only if $\psi$ is true in all elements of $M$ (resp. not true in all elements
of $M_{1}$). $N$ and $N_{1}$ serve the same purpose for defining the truth
value of $\mathbf{not}{\,}\psi$.

Satisfaction of a closed formula by a three-valued MKNF structure is defined
as follows (where $p$ is a predicate, $\psi$ is a formula, the values
$\mathtt{true}$, $\mathtt{undefined}$ and $\mathtt{false}$ follow the order
$\mathtt{false}<\mathtt{undefined}<\mathtt{true}$, and $\epsilon^{I}$
represents the individual or relation in the domain of discourse assigned to
$\epsilon$ by the interpretation $I$):

$\begin{array}[]{ll}(I,\mathcal{M},\mathcal{N})(p(t_{1},\ldots,t_{n}))&\mathtt{true}\
\textnormal{iff}\ (t_{1}^{I},\ldots,t_{n}^{I})\in p^{I}\\\ &\mathtt{false}\
\textnormal{iff}\ (t_{1}^{I},\ldots,t_{n}^{I})\not\in p^{I}\\\
(I,\mathcal{M},\mathcal{N})(\neg\psi)&\mathtt{true}\ \textnormal{iff}\
(I,\mathcal{M},\mathcal{N})(\psi)=\mathtt{false},\\\ &\mathtt{undefined}\
\textnormal{iff}\ (I,\mathcal{M},\mathcal{N})(\psi)=\mathtt{undefined},\\\
&\mathtt{false}\ \textnormal{iff}\
(I,\mathcal{M},\mathcal{N})(\psi)=\mathtt{true}\\\
(I,\mathcal{M},\mathcal{N})(\psi_{1}\wedge\psi_{2})&min\\{(I,\mathcal{M},\mathcal{N})(\psi_{1}),(I,\mathcal{M},\mathcal{N})(\psi_{2})\\}\\\
(I,\mathcal{M},\mathcal{N})(\psi_{1}\rightarrow\psi_{2})&\mathtt{true}\
\textnormal{iff}\
(I,\mathcal{M},\mathcal{N})(\psi_{1})\leq(I,\mathcal{M},\mathcal{N})(\psi_{2}),\\\
&\mathtt{false}\ \textnormal{ otherwise}\\\
(I,\mathcal{M},\mathcal{N})(\exists
x:\psi)&max\\{(I,\mathcal{M},\mathcal{N})(\psi[\alpha/x])|\alpha\in\Delta\\}\\\
(I,\mathcal{M},\mathcal{N})(\mathbf{K}\,\psi)&\mathtt{true}\ \textnormal{iff}\
(J,(M,M_{1}),\mathcal{N})(\psi)=\mathtt{true}\ \textnormal{ for all }J\in
M,\\\ &\mathtt{false}\ \textnormal{iff}\
(J,(M,M_{1}),\mathcal{N})(\psi)=\mathtt{false}\ \textnormal{ for some }J\in
M_{1},\\\ &\mathtt{undefined}\textnormal{ otherwise}\\\
(I,\mathcal{M},\mathcal{N})(\mathbf{not}{\,}\psi)&\mathtt{true}\
\textnormal{iff}\ (J,\mathcal{M},(N,N_{1}))(\psi)=\mathtt{false}\textnormal{
for some }J\in N_{1},\\\ &\mathtt{false}\ \textnormal{iff}\
(J,\mathcal{M},(N,N_{1}))(\psi)=\mathtt{true}\ \textnormal{ for all }J\in
N,\\\ &\mathtt{undefined}\textnormal{ otherwise}\end{array}$

An _MKNF interpretation_ over a universe $\Delta$ is a non-empty set of first
order interpretations over $\Delta$. An _MKNF interpretation pair_ $(M,N)$
over a universe $\Delta$ consists of two MKNF interpretations $M$, $N$ over
$\Delta$, with $\emptyset\subset N\subseteq M$. An MKNF interpretation pair
$(M,N)$ _satisfies_ a closed MKNF formula $\psi$ iff, for each $I\in M$,
$(I,(M,N),(M,N))(\psi)=\mathtt{true}$. If $M=N$, then the MKNF interpretation
pair $(M,N)$ is called _total_. If there exists an MKNF interpretation pair
satisfying $\psi$, then $\psi$ is _consistent_. An MKNF interpretation pair
$(M,N)$ over a universe $\Delta$ is a _three-valued MKNF model_ for a given
closed MKNF formula $\psi$ if

  * •

$(M,N)$ satisfies $\psi$ and

  * •

for each MKNF interpretation pair $(M^{\prime},N^{\prime})$ over $\Delta$ with
$M\subseteq M^{\prime}$ and $N\subseteq N^{\prime}$, where at least one of the
inclusions is proper and $M^{\prime}=N^{\prime}$ if $M=N$, there is
$I^{\prime}\in M^{\prime}$ such that
$(I^{\prime},(M^{\prime},N^{\prime}),(M,N))(\psi)=\mathtt{false}$. In other
words, $M$ and $N$ cannot be extended while satisfying $\psi$; the semantics
implements minimal knowledge by requiring as many possible worlds as possible.

###  2.3 Well Founded HKB Semantics

In [6], the well-founded model of an MKNF formula is defined as the three-
valued MKNF model that, intuitively, leaves as much as possible undefined. Not
all HKBs have a well-founded model; _MKNF-coherent_ HKBs [9] have a unique
well-founded model that is characterized by a partition of the atoms that
occur in rules, called the alternating fixpoint partition and defined by [6].

The NoHR query answering system [5] is based on the well-founded semantics for
HKBs.

We recall these definitions below.

An MKNF formula $\psi$ is ground if $\psi$ does not contain variables. Given a
hybrid MKNF knowledge base
$\mathcal{K}=\langle\mathcal{O},\mathcal{P}{}\rangle$, the ground
instantiation of $\mathcal{K}$ is the KB
$\mathcal{K}_{g}=\langle\mathcal{O},\mathcal{P}{}_{g}\rangle$ where
$\mathcal{P}{}_{g}$ is obtained from $\mathcal{P}$ by replacing each rule $r$
of $\mathcal{P}$ with a set of rules substituting each variable in $r$ with
constants from $\mathcal{K}$ in all possible ways. Let
$\mathcal{K}=\langle\mathcal{O},\mathcal{P}{}\rangle$ be a ground HKB. Note
that, if an HKB is DL-safe, it has the same two-valued [11] and three-valued
[6] MKNF models of its grounding over the constants that occur in it, so it
can be assumed, without loss of generality, that the HKB is ground. The set of
_known atoms_ of $\mathcal{K}$, $\mathsf{KA}({\mathcal{K}})$, is the set of
all (ground) atoms occurring in $\mathcal{P}$ [11].

######  Definition 3.

A _partition_ of $\mathsf{KA}({\mathcal{K}})$ is a pair $(P,N)$ such that
$P\subseteq N\subseteq\mathsf{KA}({\mathcal{K}})$; $(P,N)$ is _exact_ if
$P=N$.

Given $S\subseteq\mathsf{KA}({\mathcal{K}})$, the _objective knowledge of
$\mathcal{O}$ with respect to $S$_ is the set of first order formulas

$\mathsf{OB}_{{\mathcal{K}},{S}}=\\{\pi({\mathcal{O}})\\}\cup S$ (1)

where $\pi$ is the standard transformation $\pi$ for DL axioms (Table 1).

The operators $R_{\mathcal{K}}$, $D_{\mathcal{K}}$ and $T_{\mathcal{K}}$
derive atoms that are consequences of a positive HKB $\mathcal{K}$ (i.e., one
where no negative literals occur in rules) and a set $S$ of atoms.
$R_{\mathcal{K}}({S})$ is the set of immediate consequences due to rules,
i.e., the heads of rules in $\mathcal{P}$ whose bodies are composed of atoms
that are a subset of $S$; $D_{\mathcal{K}}({S})$ is the set of immediate
consequences due to axioms, i.e., the atoms from $\mathsf{KA}({\mathcal{K}})$
entailed by $\mathsf{OB}_{{\mathcal{K}},{S}}$; and
$T_{\mathcal{K}}({S})=R_{\mathcal{K}}({S})\cup D_{\mathcal{K}}({S})$. Given an
HKB $\mathcal{K}$ and a set of atoms $S\subseteq\mathsf{KA}({\mathcal{K}})$,
the following transformations, which yield positive knowledge bases, are
defined: the _MKNF transformation_ ${\mathcal{K}}/{S}$ is
$\langle{\mathcal{O}},{{\mathcal{P}}/{S}}\rangle$ where ${\mathcal{P}}/{S}$ is
the set of rules $h\leftarrow a_{1},\ldots,a_{m}$ such that there exists in
$\mathcal{P}$ a rule $h\leftarrow
a_{1},\ldots,a_{m},\sim\\!\\!b_{1},\ldots,\sim\\!\\!b_{n}$ with
$\\{b_{1},\ldots,b_{n}\\}\cap S=\emptyset$, and the _MKNF-coherent
transformation_ ${\mathcal{K}}//{S}$ is
$\langle{\mathcal{O}},{{\mathcal{P}}//{S}}\rangle$ where ${\mathcal{P}}//{S}$
is the set of rules $h\leftarrow a_{1},\ldots,a_{m}$ such that there exists in
$\mathcal{P}$ a rule $h\leftarrow
a_{1},\ldots,a_{m},\sim\\!\\!b_{1},\ldots,\sim\\!\\!b_{n}$ with
$\\{b_{1},\ldots,b_{m}\\}\cap S=\emptyset$ and
$\mathsf{OB}_{{\mathcal{K}},{S}}\not\models\neg h$.

Since, as shown in [6], $T_{\mathcal{K}}$ is monotonic if $\mathcal{K}$ is a
ground positive HKB, the following transformations of sets of atoms are well
defined: $\Gamma_{\mathcal{K}}(S)=\mathsf{lfp}({T_{{\mathcal{K}}/{S}}})$ and
$\Gamma^{\prime}_{\mathcal{K}}(S)=\mathsf{lfp}({T_{{\mathcal{K}}//{S}}})$.
Using these transformations, it is possible to define a partition of
$\mathcal{K}$’s known atoms as follows.

######  Definition 4.

For an HKB $\mathcal{K}$, the sequences of sets of atoms $\mathbf{P}$ and
$\mathbf{N}$ are defined as follows: $\mathbf{P}_{0}=\emptyset$,
$\mathbf{N}_{0}=\mathsf{KA}({\mathcal{K}})$,
$\mathbf{P}_{n+1}=\Gamma_{\mathcal{K}}(\mathbf{N}_{n})$ and
$\mathbf{N}_{n+1}=\Gamma^{\prime}_{\mathcal{K}}(\mathbf{P}_{n})$,
$\mathbf{P}_{\omega}=\bigcup\mathbf{P}_{i}$,
$\mathbf{N}_{\omega}=\bigcap\mathbf{N}_{i}$.

The pair $(\mathbf{P}_{\omega},\mathbf{N}_{\omega})$ is called $\mathcal{K}$’s
_alternating fixpoint partition_.

[9] identify the class of _MKNF-coherent_ HKBs, i.e., those whose alternating
fixpoint partition defines a well-founded model, as well as some sufficient
conditions for a HKB to be MKNF-coherent.

We assume that the HKBs that we consider are MKNF-coherent.

######  Definition 5 (MKNF-coherent HKB (Def. 10 of [9])).

An HKB $\mathcal{K}$ is _MKNF-coherent_ if $(I_{P},I_{N})$, where
$I_{P}=\\{I~{}|~{}I\models\mathsf{OB}_{{\mathcal{K}},{\mathbf{P}_{\omega}}}\\}$
and
$I_{N}=\\{I~{}|~{}I\models\mathsf{OB}_{{\mathcal{K}},{\mathbf{N}_{\omega}}}\\}$,
is a three-valued MKNF model of $\mathcal{K}$.

For MKNF-coherent HKBs, the model determined by the alternating fixpoint
partition as in Definition 5 is the unique well-founded model.

######  Proposition 1 (Proposition 2 of [9]).

If $\mathcal{K}$ is an MKNF-coherent HKB, then it has the unique well-founded
model
$(\\{I~{}|~{}I\models\mathsf{OB}_{{\mathcal{K}},{\mathbf{P}_{\omega}}}\\},\\{I~{}|~{}I\models\mathsf{OB}_{{\mathcal{K}},{\mathbf{N}_{\omega}}}\\})$

We report some sufficient conditions for MKNF-coherence from [9] in Appendix
A.

Intuitively, the alternating fixpoint partition marks each known atom in
$\mathsf{KA}({\mathcal{K}})$ and induces the well founded model.

##  3 HKBs with function symbols

In this section, we extend the language of HKBs (Section 2.2) to allow
function symbols. We define the syntax in Section 3.1 and the semantics in
Section 3.2. We also provide a running example (Example 1) of the proposed
syntax and semantics, which takes advantage of function symbols to model
natural numbers.

###  3.1 Language

The syntax extension amounts to lifting the function-free limitation of the
original HKB syntax.

######  Definition 6 (Hybrid Knowledge Base with Function Symbols).

A Hybrid Knowledge Base with Function Symbols (HKBFS) is a Hybrid Knowledge
Base (Section 2.2) whose rules can contain function applications.

The definition of DL-safety (Def. 2) also applies to HKBFSs. In this paper, we
assume that all HKBFSs are DL-safe.

######  Example 1 (Spillover).

Let $\mathcal{K}=\langle\mathcal{O},\mathcal{P}{}\rangle$, where

$\displaystyle\mathcal{P}=\ $
$\displaystyle\mathit{safe}(X)\leftarrow\sim\\!\\!{\mathit{spillover\\_count}(X,\mathit{s}(\mathit{s}(Y)))}.$
$\displaystyle\mathit{spillover\\_count}(X,\mathit{s}(Y))\leftarrow\mathit{virus}(X),\mathit{mutated}(X),\mathit{spillover\\_count}(X,Y).$
$\displaystyle\mathit{spillover\\_count}(X,0)\leftarrow\mathit{virus}(X).$
$\displaystyle\mathit{virus}(t).$ $\displaystyle\mathcal{O}=\ $
$\displaystyle\exists\mathit{mutation}.\top\sqsubseteq\mathit{mutated}$
$\displaystyle\mathit{t}:\exists\mathit{mutation}.\top$

This HKB models that $\mathit{t}$ is a virus and there is at least a mutation
of the virus $\mathit{t}$. If there exists at least one mutation for virus
$\mathit{t}$, it is mutated, and so, a spillover may have happened. Finally,
we can model the series of spillover events by means of predicate
$\mathit{spillover\\_count}$. Function $\mathit{s}(Y)$ represents the
successor of $Y$. Finally, a virus is safe if the spillover count is less than
two.

###  3.2 Iterated fixpoint HKBFS semantics

In this section, we define the semantics of an HKBFS as a partition of its
known atoms.

We proceed in a bottom-up way, similarly to [12]. In particular, we define two
inner operators (Def. 8) that, assuming sets of true and false atoms (a
3-valued interpretation for the HKBFS, Def. 7) possibly derive new true and
false atoms, respectively. These operators are monotonic in their argument
(Proposition 2), so they have a least and a greatest fixpoint, which are used
to define the outer operator (Def. 9) which updates the 3-value
interpretation. The outer operator is itself monotonic (Proposition 4), so it
has a least fixpoint, which we define (Definition 10) as the semantics of the
HKBFS.

######  Definition 7.

A 3-valued interpretation for an HKBFS $\mathcal{K}$ is a pair
$\langle{I_{\mathrm{T}}},{I_{\mathrm{F}}}\rangle$ where $I_{\mathrm{T}}$ and
$I_{\mathrm{F}}$ are disjoint sets of $\mathcal{K}$’s known atoms, i.e.,
$I_{\mathrm{T}}\subseteq\mathsf{KA}({\mathcal{K}})$,
$I_{\mathrm{F}}\subseteq\mathsf{KA}({\mathcal{K}})$, $I_{\mathrm{T}}\cap
I_{\mathrm{F}}=\emptyset$

Given a 3-valued interpretation
$\langle{I_{\mathrm{T}}},{I_{\mathrm{F}}}\rangle$, an atom $a$ is true in it
if $a\in I_{\mathrm{T}}$, false in it if $a\in I_{\mathrm{F}}$, undefined in
it otherwise.

We also define
$\langle{I_{\mathrm{T}}},{I_{\mathrm{F}}}\rangle\leq\langle{I_{\mathrm{T}}^{\prime}},{I_{\mathrm{F}}^{\prime}}\rangle$
iff $I_{\mathrm{T}}\subseteq I_{\mathrm{T}}^{\prime}$ and
$I_{\mathrm{F}}\subseteq I_{\mathrm{F}}^{\prime}$.

We denote by $\mathit{Int_{3}}^{\mathcal{K}}$ the set of 3-valued
interpretations for an HKBFS $\mathcal{K}$.

######  Definition 8.

Given a ground HKBFS $\mathcal{K}=\langle\mathcal{O},\mathcal{P}{}\rangle$,
and a 3-valued interpretation ${\cal
I}=\langle{I_{\mathrm{T}}},{I_{\mathrm{F}}}\rangle$ for $\mathcal{K}$, we
define the operators $\mathit{OpTrue}^{\mathcal{K}}_{{\cal
I}}:2^{\mathsf{KA}({\mathcal{K}})}\rightarrow 2^{\mathsf{KA}({\mathcal{K}})}$
and $\mathit{OpFalse}^{\mathcal{K}}_{{\cal
I}}:2^{\mathsf{KA}({\mathcal{K}})}\rightarrow 2^{\mathsf{KA}({\mathcal{K}})}$
as

  * •

$\mathit{OpTrue}^{\mathcal{K}}_{{\cal
I}}(\mathit{Tr})=\\{a\in\mathsf{KA}({\mathcal{K}})~{}|~{}$ there is a clause
$a\leftarrow a_{1},...,a_{n},\sim\\!\\!b_{1},\ldots,\sim\\!\\!b_{r}$ in the
grounding of $\mathcal{P}$ such that for every $i$ ($1\leq i\leq n$) $a_{i}$
is true in ${\cal I}$ or $a_{i}\in\mathit{Tr}$, and for every $j$ ($1\leq
j\leq r$) $b_{j}$ is false in ${\cal
I}\\}\cup\\{a\in\mathsf{KA}({\mathcal{K}})|\mathsf{OB}_{{\mathcal{K}},{I_{T}\cup
Tr}}\models a\\}$;

  * •

$\mathit{OpFalse}^{\mathcal{K}}_{{\cal I}}(\mathit{Fa})=$
$\\{a\in\mathsf{KA}({\mathcal{K}})~{}|~{}$
$\mathsf{OB}_{{\mathcal{K}},{I_{T}}}\models\neg a$, or, for every clause
$a\leftarrow a_{1},...,a_{n},\sim\\!\\!b_{1},\ldots,\sim\\!\\!b_{r}$ in the
grounding of $\mathcal{P}$, there is some $i$ $(1\leq i\leq n)$ such that
$a_{i}$ is false in ${\cal I}$ or $a_{i}\in\mathit{Fa}$, or there is some $j$
$(1\leq j\leq r)$ such that $b_{j}$ is true in ${\cal
I}\\}\cap\\{a\in\mathsf{KA}({\mathcal{K}})|\mathsf{OB}_{{\mathcal{K}},{\mathsf{KA}({\mathcal{K}})\setminus(I_{\mathrm{F}}\cup\mathit{Fa})}}\not\models
a\\}$

In words, $\mathit{OpTrue}^{\mathcal{K}}_{{\cal I}}(\mathit{Tr})$ represents
the true atoms that can be derived from $\mathcal{K}$ knowing ${\cal I}$ and
true atoms $\mathit{Tr}$, while $\mathit{OpFalse}^{\mathcal{K}}_{{\cal
I}}(\mathit{Fa})$ represents the false atoms that can be derived from
$\mathcal{K}$ by knowing ${\cal I}$ and false atoms $\mathit{Fa}$.

######  Proposition 2.

Given an HKBFS $\mathcal{K}$ and a 3-valued interpretation ${\cal I}$ for
$\mathcal{K}$, $\mathit{OpTrue}^{\mathcal{K}}_{{\cal I}}$ and
$\mathit{OpFalse}^{\mathcal{K}}_{{\cal I}}$ are both monotonic in their
argument.

###### Proof.

Monotonicity of $\mathit{OpTrue}^{\mathcal{K}}_{{\cal I}}$ means that if
$\mathit{Tr}\subseteq\mathit{Tr}^{\prime}$, then
$\mathit{OpTrue}^{\mathcal{K}}_{{\cal
I}}(\mathit{Tr})\subseteq\mathit{OpTrue}^{\mathcal{K}}_{{\cal
I}}(\mathit{Tr}^{\prime})$. Analogously, monotonicity of
$\mathit{OpFalse}^{\mathcal{K}}_{{\cal I}}$ means that if
$\mathit{Fa}\subseteq\mathit{Fa}^{\prime}$, then
$\mathit{OpFalse}^{\mathcal{K}}_{{\cal
I}}(\mathit{Fa})\subseteq\mathit{OpFalse}^{\mathcal{K}}_{{\cal
I}}(\mathit{Fa}^{\prime})$.

Regarding $\mathit{OpTrue}^{\mathcal{K}}_{{\cal I}}$, if
$a\in\mathit{OpTrue}^{\mathcal{K}}_{{\cal I}}(\mathit{Tr})$, Definition 8
ensures that either there is a clause $a\leftarrow
a_{1},...,a_{n},\sim\\!\\!b_{1},\ldots,\sim\\!\\!b_{r}$ in $\mathcal{P}$’s
grounding such that for each $1\leq i\leq n$ $a_{i}$ is true in ${\cal I}$ or
$a_{i}\in\mathit{Tr}$ and for each $1\leq j\leq r$ $b_{j}$ is false in ${\cal
I}$, or $\mathsf{OB}_{{\mathcal{K}},{I_{\mathrm{T}}\cup\mathit{Tr}}}\models
a$, i.e., ${\pi({\mathcal{O}})}\cup I_{\mathrm{T}}\cup\mathit{Tr}\models a$.
Since $\mathit{Tr}\subseteq\mathit{Tr}^{\prime}$, if $a_{i}\in\mathit{Tr}$,
then also $a_{i}\in\mathit{Tr}^{\prime}$, and if ${\pi({\mathcal{O}})}\cup
I_{\mathrm{T}}\cup\mathit{Tr}\models a$, then also ${\pi({\mathcal{O}})}\cup
I_{\mathrm{T}}\cup\mathit{Tr}^{\prime}\models a$ by the monotonicity of first
order logic. So $a\in\mathit{OpTrue}^{\mathcal{K}}_{{\cal
I}}(\mathit{Tr}^{\prime})$.

Regarding $\mathit{OpFalse}^{\mathcal{K}}_{{\cal I}}$, if
$a\in\mathit{OpFalse}^{\mathcal{K}}_{{\cal I}}(\mathit{Fa})$, then either

  * •

$\mathsf{OB}_{{\mathcal{K}},{I_{\mathrm{T}}}}\models\neg a$, or

  * •

for each clause $a\leftarrow
a_{1},...,a_{n},\sim\\!\\!b_{1},\ldots,\sim\\!\\!b_{r}$ in $\mathcal{P}$ there
is some $i$ $(1\leq i\leq n)$ such that either $a_{i}$ is false in ${\cal I}$
or $a_{i}\in\mathit{Fa}$ (and since
$\mathit{Fa}\subseteq\mathit{Fa}^{\prime}$, $a_{i}\in\mathit{Fa}^{\prime}$),
or some $j$ ($1\leq j\leq r$) such that $b_{j}$ is true in ${\cal I}$.

Also, if
$\mathsf{OB}_{{\mathcal{K}},{\mathsf{KA}({\mathcal{K}})\setminus(I_{F}\cup\mathit{Fa})}}\not\models
a$, then
$\mathsf{OB}_{{\mathcal{K}},{\mathsf{KA}({\mathcal{K}})\setminus(I_{\mathrm{F}}\cup\mathit{Fa}^{\prime})}}\not\models
a$ by the monotonicity of first order logic. So
$a\in\mathit{OpFalse}^{\mathcal{K}}_{{\cal I}}(\mathit{Fa}^{\prime})$. ∎

######  Proposition 3.

Given an HKBFS $\mathcal{K}$, $\mathit{OpTrue}^{\mathcal{K}}_{{\cal I}}$ and
$\mathit{OpFalse}^{\mathcal{K}}_{{\cal I}}$ are monotonic in ${\cal I}$, i.e.,
if ${\cal I}$ and ${\cal I}^{\prime}$ are three-valued interpretations for
$\mathcal{K}$ such that ${\cal I}\leq{\cal I}^{\prime}$, then

  1. 1.

for each $\mathit{Tr}\subseteq\mathsf{KA}({\mathcal{K}})$,
$\mathit{OpTrue}^{\mathcal{K}}_{{\cal
I}}(\mathit{Tr})\subseteq\mathit{OpTrue}^{\mathcal{K}}_{{\cal
I}^{\prime}}(\mathit{Tr})$

  2. 2.

for each $\mathit{Fa}\subseteq\mathsf{KA}({\mathcal{K}})$, and
$\mathit{OpFalse}^{\mathcal{K}}_{{\cal
I}}(\mathit{Fa})\subseteq\mathit{OpFalse}^{\mathcal{K}}_{{\cal
I}^{\prime}}(\mathit{Fa})$.

###### Proof.

  1. 1.

If $a\in\mathit{OpTrue}^{\mathcal{K}}_{{\cal I}}(\mathit{Tr})$, then

     * •

either there is a clause $a\leftarrow
a_{1},...,a_{n},\sim\\!\\!b_{1},\ldots,\sim\\!\\!b_{r}$ in $\mathcal{P}$’s
grounding such that for each $i$ ($1\leq i\leq n$) $a_{i}$ is true in ${\cal
I}$ (and then it is true in ${\cal I}^{\prime}$) or $a_{i}\in\mathit{Tr}$ and
for each $j$ ($1\leq j\leq r$) $b_{j}$ is false in ${\cal I}$ (and then it is
also false in ${\cal I}^{\prime}$); which would ensure
$a\in\mathit{OpTrue}^{\mathcal{K}}_{{\cal I}^{\prime}}(\mathit{Tr})$

     * •

or $\mathsf{OB}_{{\mathcal{K}},{I_{\mathrm{T}}\cup\mathit{Tr}}}\models a$,
i.e., ${\pi({\mathcal{O}})}\cup I_{\mathrm{T}}\cup\mathit{Tr}\models a$. Since
$I_{\mathrm{T}}\subseteq I_{\mathrm{T}}^{\prime}$, then also
${\pi({\mathcal{O}})}\cup
I_{\mathrm{T}}^{\prime}\cup\mathit{Tr}^{\prime}\models a$ by the monotonicity
of first order logic; which, also, would ensure
$a\in\mathit{OpTrue}^{\mathcal{K}}_{{\cal I}^{\prime}}(\mathit{Tr})$

So $a\in\mathit{OpTrue}^{\mathcal{K}}_{{\cal I}^{\prime}}(\mathit{Tr})$.

  2. 2.

If $a\in\mathit{OpFalse}^{\mathcal{K}}_{{\cal I}}(\mathit{Fa})$, then

     * •

$\mathsf{OB}_{{\mathcal{K}},{\mathsf{KA}({\mathcal{K}})\setminus(I_{\mathrm{F}}\cup\mathit{Fa})}}\not\models
a$, so also
$\mathsf{OB}_{{\mathcal{K}},{\mathsf{KA}({\mathcal{K}})\setminus(I_{\mathrm{F}}^{\prime}\cup\mathit{Fa})u}}\not\models
a$ because $I_{\mathrm{F}}^{\prime}\supseteq I_{\mathrm{F}}$ and by the
monotonicity of first order logic;

     * •

and

       * –

either $\mathsf{OB}_{{\mathcal{K}},{I_{\mathrm{T}}}}\models a$, so also
$\mathsf{OB}_{{\mathcal{K}},{I_{\mathrm{T}}^{\prime}}}\models a$ by the
monotonicity of first order logic;

       * –

or for all clauses $a\leftarrow
a_{1},...,a_{n},\sim\\!\\!b_{1},\ldots,\sim\\!\\!b_{r}$ in $\mathcal{P}$’s
grounding either there exists an $a_{i}\in I_{\mathrm{F}}\cup\mathit{Fa}$, so
$a_{i}\in I_{\mathrm{F}}^{\prime}\cup\mathit{Fa}$, or a $b_{j}\in
I_{\mathrm{T}}$, so $b_{j}\in I_{\mathrm{T}}^{\prime}$.

In conclusion, $a\in\mathit{OpFalse}^{\mathcal{K}}_{{\cal
I}^{\prime}}(\mathit{Fa})$.

∎

Given an HKBFS $\mathcal{K}$ and a 3-valued interpretation ${\cal I}$, since
$\mathit{OpTrue}^{\mathcal{K}}_{{\cal I}}$ and
$\mathit{OpFalse}^{\mathcal{K}}_{{\cal I}}$ are monotonic in their argument,
they both have least and greatest fixpoints.

So it is possible to define the following iterative operator on a 3-valued
interpretation ${\cal I}$.

######  Definition 9 (Iterated Fixed Point).

For an HKBFS $\mathcal{K}$, we define
$\mathit{IFP}^{\mathcal{K}}:\mathit{Int_{3}}^{\mathcal{K}}\rightarrow\mathit{Int_{3}}^{\mathcal{K}}$
as

$\mathit{IFP}^{\mathcal{K}}({\cal
I})=\langle{\mathsf{lfp}({\mathit{OpTrue}^{\mathcal{K}}_{{\cal
I}}})},{\mathsf{gfp}({\mathit{OpFalse}^{\mathcal{K}}_{{\cal I}}})}\rangle$.

######  Proposition 4.

For each HKBFS $\mathcal{K}$, $\mathit{IFP}^{\mathcal{K}}$ is monotonic w.r.t.
the order relation among 3-valued interpretations defined in Definition 7.

###### Proof.

Let ${\cal I}$ and ${\cal I}^{\prime}$ be two three-valued interpretations of
$\mathcal{K}$ such that ${\cal I}\leq{\cal I}^{\prime}$. By propositions 2 and
3,

  1. 1.

${\mathit{OpTrue}^{\mathcal{K}}_{{\cal
I}}}\uparrow{n}\subseteq{\mathit{OpTrue}^{\mathcal{K}}_{{\cal
I}^{\prime}}}\uparrow{n}$ for all $n$

  2. 2.

${\mathit{OpFalse}^{\mathcal{K}}_{{\cal
I}}}\downarrow{n}\subseteq{\mathit{OpFalse}^{\mathcal{K}}_{{\cal
I}^{\prime}}}\downarrow{n}$ for all $n$

Thus,

  1. 1.

$\mathsf{lfp}({\mathit{OpTrue}^{\mathcal{K}}_{{\cal
I}}})\subseteq\mathsf{lfp}({\mathit{OpTrue}^{\mathcal{K}}_{{\cal
I}^{\prime}}})$

  2. 2.

$\mathsf{gfp}({\mathit{OpFalse}^{\mathcal{K}}_{{\cal
I}}})\subseteq\mathsf{gfp}({\mathit{OpFalse}^{\mathcal{K}}_{{\cal
I}^{\prime}}})$

i.e., $\mathit{IFP}^{\mathcal{K}}({\cal
I})\leq\mathit{IFP}^{\mathcal{K}}({\cal I}^{\prime})$. ∎

By virtue of being monotonic, $\mathit{IFP}^{\mathcal{K}}$ admits a least
fixpoint for each HKBFS $\mathcal{K}$, which we define as the semantics of the
HKBFS.

######  Definition 10 (Iterated fixpoint semantics).

Given an HKBFS $\mathcal{K}$, its iterated fixpoint semantics is
$\mathsf{lfp}({\mathit{IFP}^{\mathcal{K}}})$.

######  Example 2 (Spillover cont.).

Consider the $\mathcal{K}=\langle\mathcal{O},\mathcal{P}{}\rangle$ of Example
1. Figure 1 shows the computation of the iterated fixpoint semantics for the
HKB $\mathcal{K}$. Given the presence of the function symbol
$\mathit{s}(\cdot)$, the model is infinite because there are countably many
substitutions for $\mathit{spillover\\_count}$.

$\begin{array}[]{rlrl}{I_{\mathrm{T}}}_{0}\ =&\emptyset&{I_{\mathrm{F}}}_{0}\
=&\emptyset\\\ {I_{\mathrm{T}}}_{1}\
=&\\{\mathit{virus}(\mathit{t}),&{I_{\mathrm{F}}}_{1}\
=&\mathsf{KA}({\mathcal{K}})\setminus{I_{\mathrm{T}}}_{1}\setminus\\{\mathit{safe}(t)\\}\\\
&\mathit{mutated}(\mathit{t}),&&\\\
&\mathit{spillover\\_count}(\mathit{t},0),&&\\\
&\mathit{spillover\\_count}(\mathit{t},\mathit{s}(0)),&&\\\
&\mathit{spillover\\_count}(\mathit{t},\mathit{s}(\mathit{s}(0))),&&\\\
&\cdots\\}&&\\\ {I_{\mathrm{T}}}_{2}\
=&{I_{\mathrm{T}}}_{1}&{I_{\mathrm{F}}}_{2}\
=&\mathsf{KA}({\mathcal{K}})\setminus{I_{\mathrm{T}}}_{1}\\\
{I_{\mathrm{T}}}_{3}\ =&{I_{\mathrm{T}}}_{2}&{I_{\mathrm{F}}}_{3}\
=&{I_{\mathrm{F}}}_{2}\end{array}$ Figure 1: Iterations of the
$\mathit{IFP}^{\mathcal{K}}$ operator for Example 1.

Each ${\cal I}_{m}$, for $m=1,2,3$ is determined by the fixpoints of
$\mathit{OpTrue}^{\mathcal{K}}_{{\cal I}_{m-1}}$ and
$\mathit{OpFalse}^{\mathcal{K}}_{{\cal I}_{m-1}}$ as follows.

  * •

${\mathit{OpTrue}^{\mathcal{K}}_{{\cal I}_{0}}}\uparrow{0}=\emptyset$,

  * •

${\mathit{OpTrue}^{\mathcal{K}}_{{\cal
I}_{0}}}\uparrow{1}={\mathit{OpTrue}^{\mathcal{K}}_{{\cal
I}_{0}}}\uparrow{0}\cup\\{\mathit{virus}(t),\mathit{mutated}(t)\\}$,

  * •

${\mathit{OpTrue}^{\mathcal{K}}_{{\cal
I}_{0}}}\uparrow{2}={\mathit{OpTrue}^{\mathcal{K}}_{{\cal
I}_{0}}}\uparrow{1}\cup\\{\mathit{spillover\\_count}(t,0)\\}$,

  * •

${\mathit{OpTrue}^{\mathcal{K}}_{{\cal
I}_{0}}}\uparrow{3}={\mathit{OpTrue}^{\mathcal{K}}_{{\cal
I}_{0}}}\uparrow{2}\cup\\{\mathit{spillover\\_count}(t,s(0))\\}$,

  * •

${\mathit{OpTrue}^{\mathcal{K}}_{{\cal
I}_{0}}}\uparrow{4}={\mathit{OpTrue}^{\mathcal{K}}_{{\cal
I}_{0}}}\uparrow{3}\cup\\{\mathit{spillover\\_count}(t,s(s(0)))\\}$,

and so on to the least fixpoint ${I_{\mathrm{T}}}_{1}$.

  * •

${\mathit{OpFalse}^{\mathcal{K}}_{{\cal
I}_{0}}}\downarrow{0}=\mathsf{KA}({\mathcal{K}})$

  * •

${\mathit{OpFalse}^{\mathcal{K}}_{{\cal
I}_{0}}}\downarrow{1}={\mathit{OpFalse}^{\mathcal{K}}_{{\cal
I}_{0}}}\downarrow{0}\setminus\\{\mathit{virus}(t),\mathit{mutated}(t),\mathit{safe}(t)\\}$

  * •

${\mathit{OpFalse}^{\mathcal{K}}_{{\cal
I}_{0}}}\downarrow{2}={\mathit{OpFalse}^{\mathcal{K}}_{{\cal
I}_{0}}}\downarrow{1}\setminus\\{\mathit{spillover\\_count}(t,0)\\}$

  * •

${\mathit{OpFalse}^{\mathcal{K}}_{{\cal
I}_{0}}}\downarrow{3}={\mathit{OpFalse}^{\mathcal{K}}_{{\cal
I}_{0}}}\downarrow{2}\setminus\\{\mathit{spillover\\_count}(t,s(0))\\}$

  * •

${\mathit{OpFalse}^{\mathcal{K}}_{{\cal
I}_{0}}}\downarrow{4}={\mathit{OpFalse}^{\mathcal{K}}_{{\cal
I}_{0}}}\downarrow{3}\setminus\\{\mathit{spillover\\_count}(t,s(s(0)))\\}$

and so on to the greatest fixpoint ${I_{\mathrm{F}}}_{1}$.

  * •

${\mathit{OpTrue}^{\mathcal{K}}_{{\cal I}_{1}}}\uparrow{0}=\emptyset$

  * •

${\mathit{OpTrue}^{\mathcal{K}}_{{\cal
I}_{1}}}\uparrow{1}={I_{\mathrm{T}}}_{1}$

which is the least fixpoint.

  * •

${\mathit{OpFalse}^{\mathcal{K}}_{{\cal
I}_{1}}}\downarrow{0}=\mathsf{KA}({\mathcal{K}})$

  * •

${\mathit{OpFalse}^{\mathcal{K}}_{{\cal
I}_{1}}}\downarrow{1}={\mathit{OpFalse}^{\mathcal{K}}_{{\cal
I}_{1}}}\downarrow{0}\setminus\\{\mathit{virus}(t),\mathit{mutated}(t)\\}$. In
this case, $\mathit{safe}(t)$ is kept because
$\mathit{spillover\\_count}(s(s(0)))$ is false in ${\cal I}_{1}$.

  * •

${\mathit{OpFalse}^{\mathcal{K}}_{{\cal
I}_{1}}}\downarrow{2}={\mathit{OpFalse}^{\mathcal{K}}_{{\cal
I}_{1}}}\downarrow{1}\setminus\\{\mathit{spillover\\_count}(t,0)\\}$

  * •

${\mathit{OpFalse}^{\mathcal{K}}_{{\cal
I}_{1}}}\downarrow{3}={\mathit{OpFalse}^{\mathcal{K}}_{{\cal
I}_{1}}}\downarrow{2}\setminus\\{\mathit{spillover\\_count}(t,s(0))\\}$

  * •

${\mathit{OpFalse}^{\mathcal{K}}_{{\cal
I}_{1}}}\downarrow{4}={\mathit{OpFalse}^{\mathcal{K}}_{{\cal
I}_{1}}}\downarrow{3}\setminus\\{\mathit{spillover\\_count}(t,s(s(0)))\\}$

to the greatest fixpoint
${I_{\mathrm{F}}}_{2}=\mathsf{KA}({\mathcal{K}})\setminus{I_{\mathrm{T}}}_{1}\cup\\{\mathit{safe}(\mathit{t})\\}$.

For all $m$, ${\mathit{OpTrue}^{\mathcal{K}}_{{\cal
I}_{2}}}\uparrow{m}={\mathit{OpTrue}^{\mathcal{K}}_{{\cal I}_{1}}}\uparrow{m}$
and ${\mathit{OpFalse}^{\mathcal{K}}_{{\cal
I}_{2}}}\downarrow{m}={\mathit{OpFalse}^{\mathcal{K}}_{{\cal
I}_{1}}}\downarrow{m}$, so ${\cal I}_{2}={\cal I}_{3}$ =
$\mathsf{lfp}({\mathit{IFP}^{\mathcal{K}}})$.

##  4 Properties

In this section, we prove that, for function-free HKBFSs, which are also HKBs,
Knorr et al.’s alternating fixpoint partition (def. 4) and our iterated
fixpoint (def. 10) coincide, modulo a set complement operation.

######  Theorem 1.

Given a function-free HKBFS
$\mathcal{K}=\langle\mathcal{O},\mathcal{P}{}\rangle$, let
$\mathsf{lfp}({\mathit{IFP}^{\mathcal{K}}})=\langle{I_{\mathrm{T}}},{I_{\mathrm{F}}}\rangle$.
Then $\langle{I_{\mathrm{T}}},{\mathsf{KA}({\mathcal{K}})\setminus
I_{\mathrm{F}}}\rangle$ is $\mathcal{K}$’s alternating fixpoint partition.

###### Proof.

We prove the claim by double induction. Since $\mathcal{P}$ is function-free,
its grounding is finite so all fixpoints occur at finite ordinals and it is
not necessary to consider limit ordinals.

We show by induction that
${\mathit{IFP}^{\mathcal{K}}}\uparrow{n}=\langle\mathbf{P}_{n};\mathsf{KA}({\mathcal{K}})\setminus\mathbf{N}_{n}\rangle$.

For $n=0$ (base case), $\mathit{IFP}^{\mathcal{K}}\uparrow
0=\langle{\emptyset},{\emptyset}\rangle$, while $\mathbf{P}_{0}=\emptyset$ and
$\mathbf{N}_{0}=\mathsf{KA}({\mathcal{K}})$, thus
$\langle{\mathbf{P}_{0}},{\mathsf{KA}({\mathcal{K}})\setminus\mathbf{N}_{0}}\rangle=\langle{\emptyset},{\emptyset}\rangle={\mathit{IFP}^{\mathcal{K}}}\uparrow{0}$.

For the inductive case, assume
${\mathit{IFP}^{\mathcal{K}}}\uparrow{n}=\langle{\mathbf{P}_{n}},{\mathsf{KA}({\mathcal{K}})\setminus\mathbf{N}_{n}}\rangle={\cal
I}=\langle{I_{\mathrm{T}}},{I_{\mathrm{F}}}\rangle$.

We now prove that (1) $\mathsf{lfp}({\mathit{OpTrue}^{\mathcal{K}}_{{\cal
I}}})=\mathsf{lfp}({T_{{\mathcal{K}}/{\mathsf{KA}({\mathcal{K}})\setminus
I_{\mathrm{F}}}}})$ and that (2)
$\mathsf{KA}({\mathcal{K}})\setminus(\mathsf{gfp}({\mathit{OpFalse}^{\mathcal{K}}_{{\cal
I}}}))=\mathsf{lfp}({T_{{\mathcal{K}}//{I_{\mathrm{T}}}}})$.

To prove (1), we first show by induction that
${T_{{\mathcal{K}}/{\mathsf{KA}({\mathcal{K}})\setminus
I_{\mathrm{F}}}}}\uparrow{m}\subseteq\mathit{OpTrue}^{\mathcal{K}}_{{\cal
I}}\uparrow m$.

For $m=0$ $T_{{\mathcal{K}}/{\mathsf{KA}({\mathcal{K}})\setminus
I_{\mathrm{F}}}}\uparrow 0=\emptyset$ so
$T_{{\mathcal{K}}/{\mathsf{KA}({\mathcal{K}})\setminus
I_{\mathrm{F}}}}\uparrow 0\subseteq\mathit{OpTrue}^{\mathcal{K}}_{{\cal
I}}\uparrow 0$.

For $m+1$, let $\mathit{Tr}$ be
$T_{{\mathcal{K}}/{\mathsf{KA}({\mathcal{K}})\setminus
I_{\mathrm{F}}}}\uparrow m$, and assume that
$\mathit{Tr}\subseteq{\mathit{OpTrue}^{\mathcal{K}}_{{\cal I}}}\uparrow{m}$.

If $a\in T_{{\mathcal{K}}/{\mathsf{KA}({\mathcal{K}})\setminus
I_{\mathrm{F}}}}(\mathit{Tr})$, suppose $a\in
R_{{\mathcal{K}}/{\mathsf{KA}({\mathcal{K}})\setminus
I_{\mathrm{F}}}}(\mathit{Tr})$. Then there exists a rule $a\leftarrow
l_{1},...,l_{n}$ in ${\mathcal{P}_{g}}/{\mathsf{KA}({\mathcal{K}})\setminus
I_{\mathrm{F}}}$, where $\mathcal{P}_{g}$ is the grounding of $\mathcal{P}$,
with each $l_{i}\in\mathit{Tr}$. This means that $\mathcal{P}_{g}$ contains a
rule $a\leftarrow l_{1},...,l_{n},\sim\\!\\!b_{1},\ldots,\sim\\!\\!b_{r}$ with
$b_{1},\ldots,b_{r}$ in $I_{\mathrm{F}}$. So
$a\in{\mathit{OpTrue}^{\mathcal{K}}_{{\cal I}}}\uparrow{m+1}$ by the
definition of $\mathit{OpTrue}^{\mathcal{K}}_{{\cal I}}$. If $a\in
D_{{\mathcal{K}}/{\mathsf{KA}({\mathcal{K}})\setminus
I_{\mathrm{F}}}}(\mathit{Tr})$ then $\mathsf{OB}_{{\mathcal{K}},{Tr}}\models
a$ so $a\in\mathit{OpTrue}^{\mathcal{K}}_{{\cal I}}(\mathit{Tr})$ by the
definition of $\mathit{OpTrue}^{\mathcal{K}}_{{\cal I}}$.

Since ${T_{{\mathcal{K}}/{\mathsf{KA}({\mathcal{K}})\setminus
I_{\mathrm{F}}}}}\uparrow{m}\subseteq{\mathit{OpTrue}^{\mathcal{K}}_{{\cal
I}}}\uparrow{m}$, for all $m$,
$\mathsf{lfp}({T_{{\mathcal{K}}/{\mathsf{KA}({\mathcal{K}})\setminus
I_{\mathrm{F}}}}})\subseteq\mathsf{lfp}({\mathit{OpTrue}^{\mathcal{K}}_{{\cal
I}}})$, so to prove (1) it is sufficient to show that
$\mathsf{lfp}({\mathit{OpTrue}^{\mathcal{K}}_{{\cal
I}}})\subseteq\mathsf{lfp}({T_{{\mathcal{K}}/{\mathsf{KA}({\mathcal{K}})\setminus
I_{\mathrm{F}}}}})$.

To this end, consider the sequence $S$ of sets defined by
$S_{0}=I_{\mathrm{T}}$,
$S_{m+1}=T_{{\mathcal{K}}/{\mathsf{KA}({\mathcal{K}})}\setminus
I_{\mathrm{F}}}(S_{m})$. Note that $S_{m}\subseteq S_{m+1}$ for all $m$, which
can be proved by induction. For $m=0$,
$I_{\mathrm{T}}=T_{\mathcal{K}^{\prime}}(I_{\mathrm{T}})$ where
$\mathcal{K}^{\prime}$ is a subset of
${\mathcal{K}}/{\mathsf{KA}({\mathcal{K}})\setminus I_{\mathrm{F}}}$, so if
$a\in I_{\mathrm{T}}$, then $a\in
T_{{\mathcal{K}}/{\mathsf{KA}({\mathcal{K}})}\setminus
I_{\mathrm{F}}}(I_{\mathrm{T}})=S_{1}$. For the inductive case, assume
$S_{m-1}\subseteq S_{m}$: by the monotonicity of
$T_{{\mathcal{K}}/{\mathsf{KA}({\mathcal{K}})}\setminus I_{\mathrm{F}}}$
(because of Proposition 4 of [6],
${\mathcal{K}}/{\mathsf{KA}({\mathcal{K}})\setminus I_{\mathrm{F}}}$ being
positive), $S_{m}=T_{{\mathcal{K}}/{\mathsf{KA}({\mathcal{K}})}\setminus
I_{\mathrm{F}}}(S_{m-1})\subseteq
T_{{\mathcal{K}}/{\mathsf{KA}({\mathcal{K}})}\setminus
I_{\mathrm{F}}}(S_{m})=S_{m+1}$.

We now prove by induction that ${\mathit{OpTrue}^{\mathcal{K}}_{{\cal
I}}}\uparrow{m}\subseteq S_{m}$. For $m=0$, $\emptyset\subseteq
I_{\mathrm{T}}$. Assuming the inclusion holds for a generic $m$, then if
$a\in{\mathit{OpTrue}^{\mathcal{K}}_{{\cal I}}}\uparrow{(m+1)}$, either there
is a rule $a\leftarrow
a_{1},\ldots,a_{n},\sim\\!\\!b_{1},\ldots,\sim\\!\\!b_{r}$ in
$\mathcal{P}_{g}$ with
$\\{a_{1},\ldots,a_{n}\\}\subseteq({\mathit{OpTrue}^{\mathcal{K}}_{{\cal
I}}}\uparrow{m}\cup I_{\mathrm{T}})\subseteq(S_{m}\cup S_{0})\subseteq S_{m}$
and $\\{b_{1},\ldots,b_{r}\\}\subseteq I_{\mathrm{F}}$, so
$R_{{\mathcal{K}}/{\mathsf{KA}({\mathcal{K}})}\setminus I_{\mathrm{F}}}$ can
be applied to derive $a$; or
$\mathsf{OB}_{{\mathcal{K}},{I_{\mathrm{T}}\cup{\mathit{OpTrue}^{\mathcal{K}}_{{\cal
I}}}\uparrow{m}}}$ entails $a$, but then so does
$\mathsf{OB}_{{\mathcal{K}},{S_{m}}}$, by the inductive hypothesis and because
$I_{\mathrm{T}}\subseteq S_{m}$, so
$D_{{\mathcal{K}}/{\mathsf{KA}({\mathcal{K}})}\setminus I_{\mathrm{F}}}$
applies.

Also, note that
$I_{\mathrm{T}}\subseteq\mathsf{lfp}({T_{{\mathcal{K}}/{\mathsf{KA}({\mathcal{K}})\setminus
I_{\mathrm{F}}}}})$ because $I_{\mathrm{T}}=\mathbf{P}_{n}$, $\mathbf{P}_{n}$
is the least fixpoint of a $T_{{\cal K}^{\prime}}$ operator where ${\cal
K}^{\prime}\subseteq{\mathcal{K}}/{\mathsf{KA}({\mathcal{K}})\setminus
I_{\mathrm{F}}}$, and $T_{\mathcal{K}}$ is monotonic in its (positive) HKB
argument. In fact $T_{\mathcal{K}^{\prime}}(S)\subseteq T_{\mathcal{K}}(S)$ if
$\mathcal{K}^{\prime}\subseteq\mathcal{K}$ because, if $a$ is the head of a
program rule of $\mathcal{K}^{\prime}$ whose body is true in $S$, that rule is
also in $\mathcal{K}$, and if $\mathsf{OB}_{{\mathcal{K}^{\prime}},{S}}\models
a$, then $\mathsf{OB}_{{\mathcal{K}},{S}}\models a$ by the monotonicity of
first order logic.

Moreover,
$S_{m}\subseteq\mathsf{lfp}({T_{{\mathcal{K}}/{\mathsf{KA}({\mathcal{K}})\setminus
I_{\mathrm{F}}}}})$ for all $m$. By induction:
$S_{0}=I_{\mathrm{T}}\subseteq\mathsf{lfp}({T_{{\mathcal{K}}/{\mathsf{KA}({\mathcal{K}})\setminus
I_{\mathrm{F}}}}})$. Suppose
$S_{m}\subseteq\mathsf{lfp}({T_{{\mathcal{K}}/{\mathsf{KA}({\mathcal{K}})\setminus
I_{\mathrm{F}}}}})$. Then $a\in S_{m+1}$ is the head of a rule of
${\mathcal{K}}/{\mathsf{KA}({\mathcal{K}})\setminus I_{\mathrm{F}}}$ whose
body is true in $S_{m}$. By the inductive hypothesis, it is also true in
$\mathsf{lfp}({T_{{\mathcal{K}}/{\mathsf{KA}({\mathcal{K}})\setminus
I_{\mathrm{F}}}}})$ so
$a\in\mathsf{lfp}({T_{{\mathcal{K}}/{\mathsf{KA}({\mathcal{K}})\setminus
I_{\mathrm{F}}}}})$.

Thus, $\mathsf{lfp}({\mathit{OpTrue}^{\mathcal{K}}_{{\cal
I}}})\subseteq\mathsf{lfp}({T_{{\mathcal{K}}/{\mathsf{KA}({\mathcal{K}})\setminus
I_{\mathrm{F}}}}})$, which concludes the proof of (1).

We prove (2) by proving that, for all $m$,
$T_{{\mathcal{K}}//{I_{\mathrm{T}}}}\uparrow
m=\mathsf{KA}({\mathcal{K}})\setminus(\mathit{OpFalse}^{\mathcal{K}}_{{\cal
I}}\downarrow~{}m)$.

For the base case of $m=0$, $T_{{\mathcal{K}}//{I_{\mathrm{T}}}}\uparrow
0=\emptyset$ and $\mathit{OpFalse}^{\mathcal{K}}_{{\cal I}}\downarrow
0=\mathsf{KA}({\mathcal{K}})$, so $T_{{\mathcal{K}}//{I_{\mathrm{T}}}}\uparrow
0=\mathsf{KA}({\mathcal{K}})\setminus(\mathit{OpFalse}^{\mathcal{K}}_{{\cal
I}}\downarrow 0)$.

For the inductive case, $m+1$, let $S$ be
$T_{{\mathcal{K}}//{I_{\mathrm{T}}}}\uparrow m$ and let $\mathit{Fa}$ be
${\mathit{OpFalse}^{\mathcal{K}}_{{\cal I}}}\downarrow{m}$. Note that, for all
$m$, $I_{\mathrm{F}}\subseteq{\mathit{OpFalse}^{\mathcal{K}}_{{\cal
I}}}\downarrow{m}$, because by Proposition 4
$I_{\mathrm{F}}\subseteq\mathsf{gfp}({\mathit{OpFalse}^{\mathcal{K}}_{{\cal
I}}})$; thus, $I_{\mathrm{F}}\cup\mathit{Fa}=\mathit{Fa}$.

By the inductive hypothesis,
$S=\mathsf{KA}({\mathcal{K}})\setminus(I_{\mathrm{F}}\cup\mathit{Fa})$. We now
show that, for all $a\in\mathsf{KA}({\mathcal{K}})$, $a\in
T_{{\mathcal{K}}//{I_{\mathrm{T}}}}(S)$ if and only if
$a\not\in\mathit{OpFalse}^{\mathcal{K}}_{{\cal I}}(\mathit{Fa})$.

Assume $a\in T_{{\mathcal{K}}//{I_{\mathrm{T}}}}(S)$: if
$\mathsf{OB}_{{\mathcal{K}},{S}}\models a$, then
$\mathsf{OB}_{{\mathcal{K}},{\mathsf{KA}({\mathcal{K}})\setminus(I_{\mathrm{F}}\cup\mathit{Fa})}}\models
a$, so $a\not\in\mathit{OpFalse}^{\mathcal{K}}_{{\cal I}}(\mathit{Fa})$;
otherwise, $\mathsf{OB}_{{\mathcal{K}},{I_{\mathrm{T}}}}\not\models\neg a$ and
there exists a rule $a\leftarrow
a_{1},\ldots,a_{m},\sim\\!\\!b_{1},\ldots,\sim\\!\\!b_{n}$ in
$\mathcal{P}_{g}$ such that $\\{a_{1},\ldots,a_{m}\\}\subseteq S$ and
$\\{b_{1},\ldots,b_{n}\\}\cap I_{\mathrm{T}}=\emptyset$, which, by De Morgan’s
laws and because
$S=\mathsf{KA}({\mathcal{K}})\setminus(I_{\mathrm{F}}\cup\mathit{Fa})$, is the
negation of the fact that
$\mathsf{OB}_{{\mathcal{K}},{I_{\mathrm{T}}}}\models\neg a$ or, for each rule
$a\leftarrow a_{1},\ldots,a_{m},\sim\\!\\!b_{1},\ldots,\sim\\!\\!b_{n}$ in
$\mathcal{P}_{g}$,
$\\{a_{1},\ldots,a_{m}\\}\cap(I_{\mathrm{F}}\cup\mathit{Fa})\neq\emptyset$ or
$\\{b_{1},\ldots,b_{n}\\}\cap I_{\mathrm{T}}\neq\emptyset$; so again
$a\not\in\mathit{OpFalse}^{\mathcal{K}}_{{\cal I}}(\mathit{Fa})$.

On the other hand, if $a\not\in\mathit{OpFalse}^{\mathcal{K}}_{{\cal
I}}(\mathit{Fa})$, then either $(i)$
$\mathsf{OB}_{{\mathcal{K}},{\mathsf{KA}({\mathcal{K}})\setminus(I_{\mathrm{F}}\cup\mathit{Fa})}}\models
a$ (and, since
$\mathsf{KA}({\mathcal{K}})\setminus(I_{\mathrm{F}}\cup\mathit{Fa})=S$,
$\mathsf{OB}_{{\mathcal{K}},{S}}\models a$, so $a\in
T_{{\mathcal{K}}//{I_{\mathrm{T}}}}(S)$), or $(ii$)
$\mathsf{OB}_{{\mathcal{K}},{I_{\mathrm{T}}}}\not\models\neg a$ and for a rule
$a\leftarrow a_{1},\ldots,a_{m},b_{1},\ldots,b_{n}$ in $\mathcal{P}$’s
grounding
$\\{a_{1},\ldots,a_{m}\\}\cap(I_{\mathrm{F}}\cup\mathit{Fa})=\emptyset$ (i.e.,
$\\{a_{1},\ldots,a_{m}\\}\subseteq S$) and $\\{b_{1},\ldots,b_{n}\\}\cap
I_{\mathrm{T}}=\emptyset$, so again $a\in
T_{{\mathcal{K}}//{I_{\mathrm{T}}}}(S)$. ∎

##  5 Conclusions and future work

In this paper we proposed an extension of the language of MKNF-based Hybrid
Knowledge Bases to support function symbols in rules. We extended the syntax
and proposed an iterative fixpoint semantics for the extended language. We
showed that the proposed semantics coincides with the one proposed by [6] in
the case of HKBs without function symbols, so it is an extension of it.

The proposed iterative fixpoint semantics also opens the way to the
introduction of probabilities in HKBs. We are currently working on a
probabilistic extension of HKBs with function symbols, inspired by Sato’s
distribution semantics [15], which will be based on the iterated fixpoint
operator defined in this paper. The probabilistic language of probabilistic
HKBFS will be also equipped with a query answering system, in the style of
what we did in TRILL [18, 17] and PITA [14], comparing our system with that of
Knorr and colleagues [10].

## Acknowledgements

This research was partly supported by TAILOR, a project funded by EU Horizon
2020 research and innovation programme under GA No 952215 and by the “National
Group of Computing Science (GNCS-INDAM)”.

## References

  * [1]
  * [2] Marco Alberti, Ana Sofia Gomes, Ricardo Gonçalves, João Leite & Martin Slota (2011): _Normative Systems Represented as Hybrid Knowledge Bases_.  In João Leite, Paolo Torroni, Thomas Ågotnes, Guido Boella & Leon van der Torre, editors: Computational Logic in Multi-Agent Systems - 12th International Workshop, CLIMA XII, Barcelona, Spain, Proceedings, Lecture Notes in Artificial Intelligence 6814, Springer, Berlin, pp. 330–346.  Available at http://dx.doi.org/10.1007/978-3-642-22359-4_23.
  * [3] Franz Baader, Diego Calvanese, Deborah L. McGuinness, Daniele Nardi & Peter F. Patel-Schneider, editors (2003): _The Description Logic Handbook: Theory, Implementation, and Applications_.  Cambridge University Press, New York, NY, USA, 10.1017/CBO9780511711787.
  * [4] Alex Borgida (1996): _On the relative expressiveness of description logics and predicate logics_.  Artif. Intell. 82(1-2), pp. 353–367, 10.1016/0004-3702(96)00004-5.
  * [5] Vedran Kasalica, Matthias Knorr, João Leite & Carlos Lopes (2020): _NoHR: An Overview_.  Künstliche Intell. 34(4), pp. 509–515, 10.1007/s13218-020-00650-1.
  * [6] Matthias Knorr, José Júlio Alferes & Pascal Hitzler (2011): _Local closed world reasoning with description logics under the well-founded semantics_.  Artif. Intell. 175(9-10), pp. 1528 – 1554, 10.1016/j.artint.2011.01.007.
  * [7] Hector J. Levesque (1984): _Foundations of a Functional Approach to Knowledge Representation_.  Artif. Intell. 23(2), pp. 155–212, 10.1016/0004-3702(84)90009-2.
  * [8] Vladimir Lifschitz (1991): _Nonmonotonic Databases and Epistemic Queries_.  In John Mylopoulos & Raymond Reiter, editors: 12th International Joint Conference on Artificial Intelligence (IJCAI 1991), Morgan Kaufmann, San Francisco, CA, USA, pp. 381–386.
  * [9] Fangfang Liu & Jia-Huai You (2017): _Three-valued semantics for hybrid MKNF knowledge bases revisited_.  Artificial Intelligence 252(Supplement C), pp. 123 – 138, 10.1016/j.artint.2017.08.003.  Available at http://www.sciencedirect.com/science/article/pii/S0004370217300917.
  * [10] Carlos Lopes, Matthias Knorr & João Leite (2017): _NoHR: Integrating XSB Prolog with the OWL 2 Profiles and Beyond_.  In Marcello Balduccini & Tomi Janhunen, editors: 14th International Conference on Logic Programming and Non-monotonic Reasoning (LPNMR 2017), Lecture Notes in Computer Science 10377, Springer, pp. 236–249, 10.1007/978-3-319-61660-5_22.
  * [11] Boris Motik & Riccardo Rosati (2010): _Reconciling Description Logics and Rules_.  J. ACM 57(5), pp. 30:1–30:62, 10.1145/1754399.1754403.
  * [12] Teodor C. Przymusinski (1989): _Every Logic Program Has a Natural Stratification And an Iterated Least Fixed Point Model_.  In: Proceedings of the 8th ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems (PODS-1989), ACM Press, pp. 11–21.  Available at http://doi.acm.org/10.1145/73721.73723.
  * [13] Raymond Reiter (1990): _On Asking What a Database Knows_.  In John W. Lloyd, editor: Computational Logic: Symposium Proceedings, Brussels, November 13/14, 1990, Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 96–113, 10.1007/978-3-642-76274-1_4.
  * [14] Fabrizio Riguzzi & Terrance Swift (2011): _The PITA System: Tabling and Answer Subsumption for Reasoning under Uncertainty_.  Theor. Pract. Log. Prog. 11(4–5), pp. 433–449, 10.1017/S147106841100010X.
  * [15] Taisuke Sato (1995): _A Statistical Learning Method for Logic Programs with Distribution Semantics_.  In Leon Sterling, editor: Logic Programming, Proceedings of the Twelfth International Conference on Logic Programming, Tokyo, Japan, June 13-16, 1995, MIT Press, pp. 715–729, 10.7551/mitpress/4298.003.0069.
  * [16] U. Sattler, D. Calvanese & R. Molitor (2003): _Relationships with other Formalisms_.  In: Description Logic Handbook, pp. 137–177, 10.5555/885746.885751.
  * [17] Riccardo Zese, Elena Bellodi, Fabrizio Riguzzi, Giuseppe Cota & Evelina Lamma (2018): _Tableau Reasoning for Description Logics and its Extension to Probabilities_.  Ann. Math. Artif. Intell. 82(1–3), pp. 101–130, 10.1007/s10472-016-9529-3.
  * [18] Riccardo Zese, Giuseppe Cota, Evelina Lamma, Elena Bellodi & Fabrizio Riguzzi (2019): _Probabilistic DL Reasoning with Pinpointing Formulas: A Prolog-based Approach_.  Theor. Pract. Log. Prog. 19(3), pp. 449–476, 10.1017/S1471068418000480.

##  Appendix A MKNF-coherent HKBs

We recall that the HKBs such that the alternating fixpoint partition defines a
three-valued MKNF model are called _MKNF-coherent_ [9].

From Definition 5111MKNF-coherent HKB (Def. 10 of [9]) An HKB $\mathcal{K}$ is
_MKNF-coherent_ if $(I_{P},I_{N})$, where
$I_{P}=\\{I~{}|~{}I\models\mathsf{OB}_{{\mathcal{K}},{\mathbf{P}_{\omega}}}\\}$
and
$I_{N}=\\{I~{}|~{}I\models\mathsf{OB}_{{\mathcal{K}},{\mathbf{N}_{\omega}}}\\}$,
is a three-valued MKNF model of $\mathcal{K}$.

For MKNF-coherent HKBs, the model determined by the alternating fixpoint
partition as in Definition 5 is the unique well-founded model.

From Proposition 1222Proposition 2 of [9] If $\mathcal{K}$ is an MKNF-coherent
HKB, then it has the unique well-founded model
$(\\{I~{}|~{}I\models\mathsf{OB}_{{\mathcal{K}},{\mathbf{P}_{\omega}}}\\},\\{I~{}|~{}I\models\mathsf{OB}_{{\mathcal{K}},{\mathbf{N}_{\omega}}}\\})$

For an MKNF-coherent HKB $\mathcal{K}$ with alternating fixpoint partition
$(\mathbf{P}_{\omega},\mathbf{N}_{\omega})$ and
$a\in\mathsf{KA}({\mathcal{K}})$, we write $\mathsf{WFM}(\mathcal{K})\models
a$ if $a\in\mathbf{P}_{\omega}$ and $\mathsf{WFM}(\mathcal{K})\models\neg a$
if $a\in\mathsf{KA}({\mathcal{K}})\setminus\mathbf{N}_{\omega}$.

[9] show a bijection between the three-valued MKNF models of an HKB
$\mathcal{K}$ and certain partitions of $\mathsf{KA}({\mathcal{K}})$, called
_stable partitions_. In the following, we report the definition of stable
partition and two results on stable partitions.

The definition of stable partition depends on the following evaluation scheme
of rules and logic programs w.r.t. partitions of the set of known atoms of an
HKB.

In the following, let $\mathcal{K}=\langle\mathcal{O},\mathcal{P}{}\rangle$ be
an HKB, and $T$ and $F$ two subsets of $\mathsf{KA}({\mathcal{K}})$ such that
$T\cap F=\emptyset$.

  * •

A rule $r$ in $\mathcal{P}$ is evaluated to a new rule as follows:

    * –

$r[\mathbf{K}\,,T,F]$ denotes the rule obtained by replacing each positive
literal $a$ in $r$ with $\mathtt{true}$ if $a\in T$, with $\mathtt{false}$ if
$a\in F$, and with $\mathtt{undefined}$ otherwise;

    * –

$r[\mathbf{not}{\,},T,F]$ denotes the rule obtained by replacing each negative
literal $\sim\\!\\!a$ in $r$ with $\mathtt{true}$ if $a\in F$, with
$\mathtt{false}$ if $a\in T$, and with $\mathtt{undefined}$ otherwise;

    * –

$r[T,F]$ denotes $r[\mathbf{K}\,,T,F][\mathbf{not}{\,},T,F]$.

  * •

an evaluated rule is simplified as follows:

    * –

if the value of the head atom in a rule is equal to or greater than the value
of its body, the rule is replaced by $\mathtt{true}\leftarrow$;

    * –

if the value of the head atom in a rule is less than the value of its body,
then the rule is replaced by $\mathtt{false}\leftarrow$.

  * •

A logic program is evaluated as follows:

    * –

$\mathcal{P}[\mathbf{K}\,,T,F]$, $\mathcal{P}[\mathbf{not}{\,},T,F]$,
$\mathcal{P}[T,F]$ denote the logic programs obtained by replacing each rule
$r$ in $\mathcal{P}$ with $r[\mathbf{K}\,,T,F]$, $r[\mathbf{not}{\,},T,F]$,
$r[T,F]$, respectively;

    * –

$\mathcal{P}[\mathbf{K}\,,T,F]$, $\mathcal{P}[\mathbf{not}{\,},T,F]$,
$\mathcal{P}[T,F]$ evaluate to $\mathtt{true}$ if they are empty or if all of
their rules are of the form $\mathtt{true}\leftarrow$; they evaluate to
$\mathtt{false}$ if at least one rule is of the form
$\mathtt{false}\leftarrow$.

######  Definition 11 (Stable partition – Def. 11 of [9]).

Let $\mathcal{K}$ be an HKB and $P\subseteq
N\subseteq\mathsf{KA}({\mathcal{K}})$. $(P,N)$ is a _stable partition_ of
$\mathcal{K}$ if

  1. 1.

$\mathsf{OB}_{{\mathcal{K}},{N}}$ is satisfiable;

  2. 2.

$\forall a\in\mathsf{KA}({\mathcal{K}})$, if
$\mathsf{OB}_{{\mathcal{K}},{P}}\models a$ then $a\in P$ and if
$\mathsf{OB}_{{\mathcal{K}},{N}}\models a$ then $a\in N$; and
$\mathcal{P}[P,\mathsf{KA}({\mathcal{K}})\setminus N]=\mathtt{true}$

  3. 3.

for any other partition $(P^{\prime},N^{\prime})$ with $P^{\prime}\subseteq P$
and $N^{\prime}\subseteq N$ where at least one of the inclusions is proper,
$\exists a\in\mathsf{KA}({\mathcal{K}})\setminus
P^{\prime}~{}|~{}\mathsf{OB}_{{\mathcal{K}},{P^{\prime}}}\models a$, or
$\exists a\in\mathsf{KA}({\mathcal{K}})\setminus
N^{\prime}~{}|~{}\mathsf{OB}_{{\mathcal{K}},{N^{\prime}}}\models a$, or
$\mathcal{P}[\mathbf{not}{\,},P,\mathsf{KA}({\mathcal{K}})\setminus
N][\mathbf{K}\,,P^{\prime},\mathsf{KA}({\mathcal{K}})\setminus
N^{\prime}]=\mathtt{false}$

######  Definition 12 (Induced partition (Def. 7 and Lemma 1 of [9])).

Let $S\subseteq\mathsf{KA}({\mathcal{K}})$. An MKNF interpretation pair
$(M,N)$ induces the partition $(T,P)$ of $S$ by placing each atom $a\in S$ as
follows:

  * •

$a\in T$ if and only if $\forall I\in
M,(I,({M},{N}),({M},{N}))(a)=\mathtt{true}$

  * •

$a\not\in P$ if and only if $\forall I\in
M,(I,({M},{N}),({M},{N}))(a)=\mathtt{false}$

  * •

$a\in P\setminus T$ if and only if $\forall I\in
M,(I,({M},{N}),({M},{N}))(a)=\mathtt{undefined}$

The following result establishes the correspondence between an HKB’s three-
valued models and the stable partitions of its known atoms.

######  Theorem 2 (Theorem 1 of [9]).

Let $\mathcal{K}=(\mathcal{O},\mathcal{P})$ be a hybrid MKNF KB.

  * •

If an MKNF interpretation pair $(M,N)$ is a three-valued MKNF model of
$\mathcal{K}$, then the partition $(T,P)$ of $\mathsf{KA}({\mathcal{K}})$
induced by $(M,N)$ is a stable partition of ${\cal K}$.

  * •

If a partition $(T,P)$ is a stable partition of $\mathcal{K}$, then the
interpretation pair $(M,N)$, where
$(M,N)=(\\{I~{}|~{}I\models\mathsf{OB}_{{\mathcal{K}},{T}}\\},\\{I~{}|~{}I\models\mathsf{OB}_{{\mathcal{K}},{P}}\\})$,
is a three-valued MKNF model of $\mathcal{K}$.

The following theorem shows that, for certain HKBs, the alternating fixpoint
partition is stable, so it defines a three-valued model which, by Theorem 2,
is the HKB’s unique well-founded model.

######  Theorem 3 (Theorem 3 of [9]).

Let $\mathcal{K}=(\mathcal{O},\mathcal{P})$ be a hybrid MKNF KB.

  * •

Assume $\pi({\mathcal{O}})$ is satisfiable. Then, for any
$E\subseteq\mathsf{KA}({\mathcal{K}})$, $(E,E)$ is a stable partition of
$\mathsf{KA}({\mathcal{K}})$ iff
$E=\Gamma_{\mathcal{K}}(E)=\Gamma^{\prime}_{\mathcal{K}}(E)$.

  * •

Assume $\mathcal{K}$ is MKNF-coherent. Then, for any partition $(T,P)$ of
$\mathsf{KA}({\mathcal{K}})$, $(T,P)$ is a stable partition of $\mathcal{K}$
iff $T=\Gamma_{\mathcal{K}}(P)$ and $P=\Gamma^{\prime}_{\mathcal{K}}(T)$.