text:
\section{Introduction}
\label{sec:introduction}

In the last years, Answer Set Programming (ASP) has emerged as an
increasingly popular approach to declarative problem solving for a range
of applications \cite{brew-etal-11-asp}, thanks to expressive and
efficient systems like \smodels{}~\cite{simo-etal-2002},
\dlv{}~\cite{leon-etal-06-dlv}, cmodels~\cite{glm2006-jar}, and
\clasp{}~\cite{gks2012-aij}. However, recent developments in computing,
in which context awareness, distribution and heterogeneous information
sources gain importance, raised the need for access to external sources
in programs, be it in the context of the Web to access web services,
databases, or ontological information in different formats, in the
context of agents to acquire sensor input, etc.

To cater for this need, \hex{}-programs~\cite{eist2005} extend ASP
with so called external atoms, through which the user can couple any
external data source with a logic
program.  Roughly, such atoms pass information from the program, given
by predicate extensions, into an external source which
returns output values of an (abstract) function that it computes.
This extension has been utilized for a range of applications,
including querying data and ontologies on the Web,
multi-context reasoning, and reasoning about actions and planning, to mention a few
(cf.\ \cite{efiks2011-lpnmr}).
Notably, recursive data exchange between the rules and the external
sources is supported, which makes the formalism powerful.

The semantics of a \hex{}-program $\ensuremath{\Pi}$ is
defined in terms of answer sets based on the  FLP reduct~\cite{flp2011-ai}:
an interpretation $\ensuremath{\mathbf{A}}$ is an answer set of $\ensuremath{\Pi}$, if and
only if it
is a~$\subseteq$-minimal model of the FLP-reduct $f\ensuremath{\Pi}^{\ensuremath{\mathbf{A}}}$ of $\ensuremath{\Pi}$ wrt.\ $\ensuremath{\mathbf{A}}$,
which is the set of all rules whose body is satisfied by $\ensuremath{\mathbf{A}}$.
For ordinary logic programs, this semantics coincides with the one
where the canonical  GL-reduct \cite{gelf-lifs-91} is in place of
$f\ensuremath{\Pi}^{\ensuremath{\mathbf{A}}}$, and it is more appealing for extensions
with nonmonotonic aggregates \cite{flp2011-ai}, and the more general external atoms in \hex-programs.

The evaluation of a \hex-program $\ensuremath{\Pi}$ in the \dlvhex{}\footnote{\url{http://www.kr.tuwien.ac.at/research/systems/dlvhex/}} solver
proceeds in two steps as
follows. In Step~1, external atoms are
viewed as ordinary atoms (\emph{replacement atoms}) and their truth
values are guessed by choice rules that are added. The resulting ordinary ASP program $\ensuremath{\hat{\Pi}}$ is
then evaluated by an ordinary ASP solver and each of its answer sets $\ensuremath{\hat{\mathbf{A}}}$
is checked against the external sources, i.e., the guess is
verified. After that, the guess
for the non-replacement atoms, called $\ensuremath{\mathbf{A}}$, is known to be a
model of $\ensuremath{\Pi}$, and thus also of the reduct $f\ensuremath{\Pi}^{\ensuremath{\mathbf{A}}}$.  Step~2 then checks whether $\ensuremath{\mathbf{A}}$ is
a $\subseteq$-minimal model  or, equivalently,
whether $\ensuremath{\mathbf{A}}$ is unfounded-free \cite{faber2005-lpnmr}, i.e.,
there exists no unfounded set (UFS) of $\ensuremath{\Pi}$ wrt.~$\ensuremath{\mathbf{A}}$.

Unfortunately, Step 2 is computationally expensive in general, and it is
intractable even for Horn programs with nonmonotonic external atoms of
polynomial complexity, as follows from results in \cite{flp2011-ai}.
It is thus worthwhile to be aware of cases where this test is tractable,
or even better, superfluous such that Step~2 can be skipped.

Motivated by this issue, we consider in this paper programs $\ensuremath{\Pi}$
for which the result of Step~1 is a $\subseteq$-minimal model of the
reduct $f\ensuremath{\Pi}^{\ensuremath{\mathbf{A}}}$.
We provide a sound \emph{syntactic criterion}
for deciding whether  the minimality check is needed,
and in further elaboration, we describe how a program can be
\emph{decomposed} into program components such that unfoundedness checks
can be delegated to the components, and the necessity of Step~2 thus be
assessed on a finer-grained level.

More in detail, our main contributions are the following:

\begin{myitemize}
\item We present a \emph{syntactic decision criterion} which can be used
  to decide whether a program possibly has unfounded sets. If the result
  of this check is negative, then the computationally expensive search
  for unfounded sets can be skipped. The criterion is based on atom
  dependency and, loosely speaking states that there are no cyclic
  dependencies of ground atoms through external atoms. This criterion
  can be efficiently checked for a given ground \hex{}-program using
  standard methods, and in fact applies to a range of applications, in
  particular, for input-stratified programs, where external sources are
  accessed in a workflow to produce input for the next stage of
  computation. However, there are relevant applications of
  \hex{}-programs where cycles through external atoms are essential,
  e.g., in encodings of problems on multi-context systems \cite{be2007} or abstract
  argumentation systems ~\cite{dung1995-aij}, for which Step~2 cannot be skipped.

\item In further elaboration, we consider a \emph{decomposition} of
  a program $\ensuremath{\Pi}$ into components based on the dependency graph
  that is induced by the program. We show that~$\ensuremath{\Pi}$ has some
  unfounded set with respect to the candidate answer set $\ensuremath{\mathbf{A}}$
  if and only if (at least) one of the components $\ensuremath{\Pi}_C$ in the
  decomposition has some unfounded set wrt.\ $\ensuremath{\mathbf{A}}$; note that
  computing the decomposition is efficiently possible, and thus does not
  incur a large overhead. This allows us to apply the decision
  criterion for the necessity of Step~2 efficiently on a more fine-grained level, and
  the search for unfounded sets can be guided to relevant parts of the
  program. In particular, for the \hex{}-encoding of a Dung-style
  argumentation semantics \cite{dung1995-aij} which we consider, the decomposition
  approach yields a considerable gain, as shown in a preliminary experimental evaluation.
\end{myitemize}

This paper complements recent work on unfoundedness
checking for \hex{}-programs in~\cite{efkrs2012-jelia,eite-etal-12a}, which is part
of a larger effort to provide efficient evaluation of \hex{}-programs,
based on new algorithms cf.\ \cite{efkr2012-tplp}. By their wide
applicability, our results are significant especially for many
potential applications in practice.

\section{Preliminaries}
\label{sec:preliminaries}

In this section, we
start with some basic definitions, and then
introduce syntax and semantics of \hex{}-programs
and the notion of unfounded sets we are going to use.

A  \emph{(signed) literal}\/ is a positive or a negative formula
$\mathbf{T} a$ resp.\ $\mathbf{F} a$, where $a$ is a ground atom of form $p(c_1, \dotsc, c_\ell)$,
with predicate $p$ and %
constants
$c_1, \dotsc, c_\ell$,
abbreviated %
$p(\vec{c})$.
For a literal $\sigma \eqs \mathbf{T} a$ or $\sigma \eqs \mathbf{F} a$,
let $\overline{\sigma}$ denote its
opposite,
i.e., $\overline{\mathbf{T} a} \eqs \mathbf{F} a$ and $\overline{\mathbf{F} a} \eqs \mathbf{T} a$.

An \emph{assignment}\/ %
is a consistent set of literals
$\mathbf{T} a$ or $\mathbf{F} a$, where $\mathbf{T} a$ expresses that~$a \ins \mathcal{A}$
and
$\mathbf{F} a$ that %
$a \notins \mathcal{A}$.
$\mathcal{A}$ is \emph{complete}, also called an \emph{interpretation\/},
if no assignment $\ensuremath{\mathbf{A}}' \supsets \ensuremath{\mathbf{A}}$ exists.
We denote by $\ensuremath{\mathbf{A}}^{\mathbf{T}} \eqs \{ a \mid \mathbf{T} a \ins \ensuremath{\mathbf{A}} \}$
and $\ensuremath{\mathbf{A}}^{\mathbf{F}} \eqs \{ a \mid \mathbf{F} a \ins \ensuremath{\mathbf{A}} \}$
the set of atoms that are true, resp.\ false in $\ensuremath{\mathbf{A}}$, and
by $\mathit{ext}(q, \ensuremath{\mathbf{A}}) =
\{ \vec{c} \mid \mathbf{T} q(\vec{c}) \ins \ensuremath{\mathbf{A}} \}$
the extension of a predicate $q$.
Furthermore, ${\ensuremath{\mathbf{A}}}|_{q}$ is the set of all literals over
atoms of form $q(\vec{c})$ in $\ensuremath{\mathbf{A}}$. For a list $\vec{q} =
q_1,\dotsc,q_k$ of predicates we write $p \in \vec{q}$ iff $q_i = p$
for some $1 \le i \le k$, and let~${\ensuremath{\mathbf{A}}}|_{\vec{q}}
= \bigcup_{j} {\ensuremath{\mathbf{A}}}|_{q_j}$.

A \emph{nogood} is a set $\{ L_1, \dotsc, L_n \}$ of
literals
$L_i, 1 \le i \le n$.
An interpretation $\ensuremath{\mathbf{A}}$ is a \emph{solution} to a nogood $\delta$
(resp.\ a set $\Delta$ of nogoods), iff $\delta \not\subseteq \ensuremath{\mathbf{A}}$
(resp.\ $\delta \not \subseteq \ensuremath{\mathbf{A}}$ for all $\delta \in \Delta$).

\subsection{\hex-Programs}

\hex-programs were introduced
in~\cite{eist2005} as a generalization of (disjunctive)
extended logic programs under the answer set
semantics~\cite{gelf-lifs-91};
for details and background see~\cite{eist2005}.

\leanparagraph{Syntax}
\hex-programs extend ordinary ASP programs by \emph{external atoms},
which enable a bidirectional interaction between a program
and external sources of computation.
External atoms have a list of input parameters (constants or predicate names)
and a list of output parameters. Informally,
to evaluate an external atom, the reasoner passes the constants and extensions of the predicates
in the input tuple to the external source
associated with the external atom.
The external source
computes %
output tuples which are matched
with the output list. More formally,
a \emph{ground external atom} is of the form
\begin{equation}
\label{grexat}
\ext{g}{\vec{p}}{\vec{c}},
\end{equation}
where
$\vec{p} = p_1, \dotsc, p_k$ are constant input parameters (predicate names or object constants),
and
$\vec{c} = c_1, \dotsc, c_l$ are
constant output terms.

Ground \hex-programs are then defined similar to ground ordinary ASP programs.

\begin{definition}[Ground \hex-programs]
A ground \hex-program consists of rules
\begin{equation}
\label{rule}
  a_1\lor\cdots\lor a_k \leftarrow b_1,\dotsc, b_m, \naf\, b_{m+1},
  \dotsc, \naf\, b_n \ ,
\end{equation}
where each $a_i$ is an (ordinary) ground atom $p(c_1,\dotsc,c_\ell)$
with constants $c_i$, $1 \le i \le \ell$,
each~$b_j$ is either an ordinary ground atom or a ground external atom,
and $k+n>0$.%
\footnote{
For simplicity, we do not formally introduce strong negation
but view, as customary, classical literals $\neg a$ as new atoms
together with a constraint $\leftarrow a, \neg a$.
}
\end{definition}

The \emph{head} of a rule $r$ is
$H(r) = \{a_1, \dotsc, a_n \}$ and
the \emph{body}
is $B(r) = \{b_1, \dotsc, b_m,$ $\naf\, b_{m+1}, \dotsc, \naf\, b_n\}$.
We call $b$ or $\naf b$ in a rule body a \emph{default literal};
$B^{+}(r) = \{b_1, \dotsc, b_m\}$ is the \textit{positive body},
$B^{-}(r) = \{b_{m+1}, \dotsc, b_n\}$ is the \textit{negative body}.
For a program $\ensuremath{\Pi}$, let $A(\ensuremath{\Pi})$ be the set of all ordinary atoms occurring in $\ensuremath{\Pi}$.

We also use non-ground programs.
However, as suitable safety conditions allow for
using a grounding procedure \cite{eist2006},
we limit our investigation to ground programs.

\leanparagraph{Semantics and Evaluation}
Intuitively, a ground external atom $\ext{g}{\vec{p}}{\vec{c}}$
is true, if the external source $\amp{g}$ yields output tuple $\vec{c}$
when evaluated with input $\vec{p}$.
Formally, the semantics of a ground external atom $\ext{g}{\vec{p}}{\vec{c}}$
wrt.~an interpretation $\ensuremath{\mathbf{A}}$ is given by the value of a $1{+}k{+}l$-ary Boolean
\emph{oracle function} $\extfun{g}$ that is defined for all possible values
of $\ensuremath{\mathbf{A}}$, $\vec{p}$ and $\vec{c}$,
where $k$ is the length of $\vec{p}$ and $l$ is the length of $\vec{c}$.  Thus,
$\ext{g}{\vec{p}}{\vec{c}}$ is true relative
to $\ensuremath{\mathbf{A}}$ if and only if it holds that
$\extsem{g}{\ensuremath{\mathbf{A}}}{\vec{p}}{\vec{c}} = 1$.
Satisfaction of ordinary  rules and ASP programs~\cite{gelf-lifs-91}
is then extended to
\hex-rules and programs in the obvious way, and
the notion of extension $\mathit{ext}(\cdot, \ensuremath{\mathbf{A}})$
for external predicates $\amp{g}$ with input lists $\vec{p}$
is naturally defined by
$\mathit{ext}(\amp{g}[\vec{p}], \ensuremath{\mathbf{A}}) =
\{ \vec{c} \mid \extsem{g}{\ensuremath{\mathbf{A}}}{\vec{p}}{\vec{c}} = 1\}$.

\begin{definition}[FLP-Reduct~\cite{flp2011-ai}]
\label{def:flpreduct}
For an interpretation $\ensuremath{\mathbf{A}}$ over a program $\ensuremath{\Pi}$, the \emph{FLP-reduct}
$f\ensuremath{\Pi}^{\ensuremath{\mathbf{A}}}$ of $\ensuremath{\Pi}$ wrt.\ $\ensuremath{\mathbf{A}}$ is the set
$\{ r \in \ensuremath{\Pi} \mid \ensuremath{\mathbf{A}} \models b, \mbox{ for all } b \in B(r) \}$
of all rules whose body is satisfied under $\ensuremath{\mathbf{A}}$.
\end{definition}

An assignment $\ensuremath{\mathbf{A}}_1$ is smaller or equal to another assignment $\ensuremath{\mathbf{A}}_2$
wrt.~a program $\ensuremath{\Pi}$, denoted $\ensuremath{\mathbf{A}}_1 \leq_\ensuremath{\Pi} \ensuremath{\mathbf{A}}_2$ iff
$\{ \mathbf{T} a \in \ensuremath{\mathbf{A}}_1^{\mathbf{T}} \mid a \in A(\ensuremath{\Pi}) \} \subseteq \{ \mathbf{T} a \in \ensuremath{\mathbf{A}}_2^{\mathbf{T}} \mid a \in A(\ensuremath{\Pi}) \}$.
\begin{definition}[Answer Set]
\label{def:answerset}
An answer set of $\ensuremath{\Pi}$ is a $\leq_\ensuremath{\Pi}$-minimal (complete) model $\ensuremath{\mathbf{A}}$ of
$f \ensuremath{\Pi}^\ensuremath{\mathbf{A}}$.
\end{definition}

Since interpretations (and thus answer sets, etc.) are complete assignments, slightly abusing
notation, we adopt the usual convention to uniquely identify them with the set of
all positive literals they contain.

\begin{example}
\label{ex:id}
Consider the program $\ensuremath{\Pi}%
  = \{
  p %
  \leftarrow \ext{\mathit{id}}{p}{}
  \}$,
where $\ext{\mathit{id}}{p}{}$ is true iff~$p$ is true. Then
$\ensuremath{\Pi}$ has the answer set $\ensuremath{\mathbf{A}}_1 = \emptyset$,
which is indeed %
a $\leq_\ensuremath{\Pi}$-minimal model of~$f \ensuremath{\Pi}^{\ensuremath{\mathbf{A}}_1} = \emptyset$.
\end{example}
The answer sets of a \hex-program $\ensuremath{\Pi}$ are
determined by the \dlvhex{} solver using a transformation
to ordinary ASP programs as follows.
Each external atom
$\ext{g}{\vec{p}}{\vec{c}}$
in~$\ensuremath{\Pi}$ is replaced by an ordinary ground \emph{external replacement atom}
$e_{\amp{g}[\vec{p}]}(\vec{c})$
and a rule~
$e_{\amp{g}[\vec{p}]}(\vec{c}) \vee \mathit{ne}_{\amp{g}[\vec{p}]}(\vec{c}) \leftarrow$
is added to the program. The answer sets of the resulting \emph{guessing program} $\ensuremath{\hat{\Pi}}$
are determined by an ordinary ASP solver and projected
to non-replacement atoms.
However, the resulting
interpretations are not necessarily models
of $\ensuremath{\Pi}$, as the value of
$\amp{g}[\vec{p}]$ under $f_{\amp{g}}$
can be different from the one of $e_{\amp{g}[\vec{p}]}(\vec{c})$.
Each answer set of $\ensuremath{\hat{\Pi}}$ is thus merely a \emph{candidate} %
which must be checked against the external sources.
If no discrepancy is found, the model candidate is a
\emph{compatible set} of~$\ensuremath{\Pi}$. More precisely,
\begin{definition}[Compatible Set]
\label{def:compatibleset}
A \emph{compatible set} of a program $\ensuremath{\Pi}$
is an interpretation~$\ensuremath{\hat{\mathbf{A}}}$  such that
\begin{compactenum}[(i)]
\item\label{en:cs1} $\ensuremath{\hat{\mathbf{A}}}$ is an answer set \cite{gelf-lifs-91} of the \emph{guessing program}
$\ensuremath{\hat{\Pi}}$, and
\item\label{en:cs2} $\extsem{g}{\ensuremath{\hat{\mathbf{A}}}}{\vec{p}}{\vec{c}} = 1$ iff
$\mathbf{T} e_{\amp{g}[\vec{p}]}(\vec{c}) \in \ensuremath{\hat{\mathbf{A}}}$ for
all external atoms $\amp{g}[\vec{p}](\vec{c})$ in $\ensuremath{\Pi}$,
i.e. the guessed values coincide with the actual output
under the input from $\ensuremath{\hat{\mathbf{A}}}$.
\end{compactenum}
\end{definition}
The compatible sets of $\Pi$ %
include (modulo
$A(\Pi)$) all (FLP) answer sets.
For each answer set $\ensuremath{\mathbf{A}}$ there is a compatible set
$\ensuremath{\hat{\mathbf{A}}}$ such that $\ensuremath{\mathbf{A}}$ is the restriction of
$\ensuremath{\hat{\mathbf{A}}}$ to non-replacement atoms, but not vice versa.
To filter out the compatible sets which are not answer sets,
the current evaluation algorithm
proceeds as follows.
Each compatible set $\ensuremath{\mathbf{A}}$ is fed to the minimality check,
which is realized as a search for unfounded sets.
This is justified by
the following
Definitions~\ref{def:unfoundedset}~and~\ref{def:unfoundedfree}
and Theorem~\ref{def:answersetsufs} from~\cite{efkrs2012-jelia}.
(These results lift unfounded sets for disjunctive logic programs
with arbitrary aggregates~\cite{faber2005-lpnmr} to \hex{}-programs.)

\begin{definition}[Unfounded Set~\cite{efkrs2012-jelia}]
\label{def:unfoundedset}
Given a program $\Pi$ and an interpretation $\ensuremath{\mathbf{A}}$, let $X$
be any set of ordinary ground atoms appearing in $\Pi$. Then,
$X$ is an \emph{unfounded set for %
$\ensuremath{\mathbf{A}}$} iff, for each rule $r$ having some atoms
from $X$ in the head,
at least one of the following conditions holds,
where $\ensuremath{\mathbf{A}} \ensuremath{\stackrel{.}{\cup} \neg .} X = (\ensuremath{\mathbf{A}} \setminus \{ \mathbf{T} a \mid a \in X\}) \cup \{ \mathbf{F} a \mid a \in X\}$:
\begin{compactenum}[(i)]
\item some literal of $B(r)$ is false wrt.~$\ensuremath{\mathbf{A}}$,
\item some literal of $B(r)$ is false wrt.~$\ensuremath{\mathbf{A}} \ensuremath{\stackrel{.}{\cup} \neg .} X$, or
\item some atom of $H(r) \setminus X$ is true wrt.~$\ensuremath{\mathbf{A}}$.
\end{compactenum}
\end{definition}

\begin{definition}[Unfounded-free Interpretations~\cite{efkrs2012-jelia}]
\label{def:unfoundedfree}
An interpretation $\ensuremath{\mathbf{A}}$ of a program~$\ensuremath{\Pi}$ is \emph{unfounded-free}
iff $\ensuremath{\mathbf{A}}^{\mathbf{T}} \cap X = \emptyset$, for all unfounded sets $X$ of $\ensuremath{\Pi}$ wrt.~$\ensuremath{\mathbf{A}}$.
\end{definition}

\begin{theorem}[Characterization of Answer Sets~\cite{efkrs2012-jelia}]
\label{def:answersetsufs}
A model $\ensuremath{\mathbf{A}}$ of a program $\ensuremath{\Pi}$ is an answer set iff
it is \emph{unfounded-free}.
\end{theorem}

\begin{example}[cont'd]
\label{ex:id-contd}
Reconsider the program $\ensuremath{\Pi} = \{\, p \leftarrow \ext{\mathit{id}}{p}{}\,\}$
from above.
Then the corresponding guessing program is
$\ensuremath{\hat{\Pi}}
  = \{
  p %
  \leftarrow e_{\amp{\mathit{id}}[p]}();
  e_{\amp{\mathit{id}}[p]}{} \vee \mathit{ne}_{\amp{\mathit{id}}[p]}{}
  \leftarrow
  \}$
and has the answer sets $\ensuremath{\mathbf{A}}_1 = \emptyset$ and
$\ensuremath{\mathbf{A}}_2 = \{\mathbf{T} p, \mathbf{T}  e_{\amp{\mathit{id}}[p]}{}\}$.
While $\ensuremath{\mathbf{A}}_1$ does not intersect with any unfounded sets and
is thus also a $\leq_\ensuremath{\Pi}$-minimal model of $f \ensuremath{\Pi}^{\ensuremath{\mathbf{A}}_1} = \emptyset$, $A_2$ intersects with the unfounded set $U = \{p\}$ and is not an answer set.
\end{example}

Our \hex{} implementation \dlvhex{} realizes
the search for unfounded sets as a separate search
problem using an encoding as a SAT instance. That is,
for a program $\ensuremath{\Pi}$ and an interpretation $\ensuremath{\mathbf{A}}$
we construct a set of nogoods $\Gamma_{\ensuremath{\Pi}}^{\ensuremath{\mathbf{A}}}$
such that its solutions contain representations of all unfounded sets
of $\ensuremath{\Pi}$ wrt.~$\ensuremath{\mathbf{A}}$. A (relatively simple) post-check
finds the unfounded sets among the solutions of $\Gamma_{\ensuremath{\Pi}}^{\ensuremath{\mathbf{A}}}$.

\section{Deciding the Necessity of the UFS Check}
\label{sec:decisioncriterion}

An alternative to the search for unfounded sets is an explicit construction
of the reduct and a search for smaller models.
However, it turned out that the minimality check based on unfounded sets
is more efficient. Nevertheless the computational costs are still high.
Moreover, during evaluation of $\ensuremath{\hat{\Pi}}$ for computing the
compatible set $\ensuremath{\hat{\mathbf{A}}}$, the ordinary ASP solver has already
made an unfounded set check, and we can safely assume that
it is founded from its perspective. Hence, all remaining unfounded
sets which were not discovered by the ordinary ASP solver have to
involve external sources, as their behavior is not fully
captured by the ASP solver.

In this section we formalize these ideas and
define a decision criterion which allows us to decide whether
a further UFS check is necessary for a given program.
We eventually define a class of programs which does not require
an additional unfounded set check.
Intuitively, we show that
every unfounded
set that is not already detected during the construction of $\ensuremath{\hat{\mathbf{A}}}$
contains input atoms of external atoms which are involved in cycles.
If no such input atom exists in the program, then the UFS check
is superfluous.

Let us therefore start with a definition of atom dependency.
\begin{definition}[Atom Dependency]
\label{def:atomdependency}
For a ground program $\ensuremath{\Pi}$, and ground atoms $p(\vec{c})$ and $q(\vec{d})$,
we say that
\begin{compactenum}[(i)]
\item $p(\vec{c})$ \emph{depends} on $q(\vec{d})$, denoted $p(\vec{c}) \rightarrow q(\vec{d})$,
	iff for some rule $r \in \ensuremath{\Pi}$ we have $p(\vec{c}) \in H(r)$ and $q(\vec{d}) \in B^{+}(r)$;
\item $p(\vec{c})$ \emph{depends externally} on $q(\vec{d})$, denoted $p(\vec{c}) \rightarrow_e q(\vec{d})$,
	iff for some rule $r \in \ensuremath{\Pi}$ we have $p(\vec{c}) \in H(r)$ and there is a $\amp{g}[q_1, \ldots, q_n](\vec{e}) \in B^{+}(r) \cup B^{-}(r)$ with $q_i = q$ for some $1 \le i \le n$.
\end{compactenum}
\end{definition}

In the following, we consider \emph{dependency graphs} $G^R_{\ensuremath{\Pi}}$ for a ground program
$\ensuremath{\Pi}$, where the set of vertices is the set of all ground atoms, and the set of edges
is given by a binary relation $R$ over ground atoms. If $R$ is not explicitly mentioned, then it
is assumed to consist of $\rightarrow \cup \rightarrow_e$, whose elemtents are also
called \emph{ordinary edges} and \emph{e-edges}, respectively.

The next definition and lemma allow to restrict our attention to the ``core'' of an unfounded set,
i.e., its most essential part. For our purpose, we can then focus on such cores, disregarding atoms
in a cut which is defined as follows.
\begin{definition}[Cut]
\label{def:cut}
Let $U$ be an unfounded set of $\ensuremath{\Pi}$ wrt.~$\ensuremath{\mathbf{A}}$.
A set of atoms $C \subseteq U$ is called a \emph{cut}, iff
\begin{compactenum}[(i)]
\item $b \not \rightarrow_e a$,  for all $a \in C$ and $b \in U$ ($C$
  has no incoming or internal e-edges), and
\item $b \not \rightarrow a$ and $a \not \rightarrow b$, for all $a \in C$ and $b \in U \setminus C$ (there are no ordinary edges between $C$ and $U \setminus C$).
\end{compactenum}
\end{definition}
\begin{example}
\label{ex:cut}
Consider the program $\ensuremath{\Pi}$ given as the following set of rules
\begin{align*}
r &\leftarrow \ext{\mathit{id}}{r}{} \\
p &\leftarrow \ext{\mathit{id}}{r}{}\\
p &\leftarrow q\\
q &\leftarrow p
\end{align*}
We have $p \rightarrow q$, $q \rightarrow p$, $r \rightarrow_e r$ and $p \rightarrow_e r$.
Program $\ensuremath{\Pi}$ has the unfounded set~$U = \{p,q,r\}$ wrt.~$\ensuremath{\mathbf{A}} = \{ \mathbf{T} p, \mathbf{T} q, \mathbf{T} r\}$.
Observe that $C = \{p,q\}$ is a cut, and therefore we have that~$U \setminus C = \{r\}$
is an unfounded set of $\ensuremath{\Pi}$ wrt.~$\ensuremath{\mathbf{A}}$.
\end{example}

We first prove that cuts can be removed from unfounded sets and the
resulting set is still an unfounded set.
\begin{lemma}[Unfounded Set Reduction Lemma]
\label{lemma:ufsreduction}
Let $U$ be an unfounded set of $\ensuremath{\Pi}$ wrt.~$\ensuremath{\mathbf{A}}$, and let $C$ be a cut.
Then, $Y = U \setminus C$ is an unfounded set of $\ensuremath{\Pi}$ wrt.~$\ensuremath{\mathbf{A}}$.
\end{lemma}
\begin{proofsketch}
If $Y = \emptyset$, then the result holds trivially.
Otherwise,
let $r \in \ensuremath{\Pi}$ with $H(r) \cap Y \not= \emptyset$. We show that one of the conditions
in Definition~\ref{def:unfoundedset} holds.
Observe that $H(r) \cap U \not= \emptyset$ because $U \supseteq Y$.
Since $U$ is an unfounded set of $\ensuremath{\Pi}$ wrt.~$\ensuremath{\mathbf{A}}$, either
\begin{compactenum}[(i)]
\item $\ensuremath{\mathbf{A}} \not \models b$ for some $b \in B(r)$; or
\item $\ensuremath{\mathbf{A}} \ensuremath{\stackrel{.}{\cup} \neg .} U \not \models b$ for some $b \in B(r)$; or
\item $\ensuremath{\mathbf{A}} \models h$ for some $h \in H(r) \setminus U$
\end{compactenum}
If (i), then the condition also holds wrt.~$Y$.

If (ii), let $a \in H(r)$ such that $a \in Y$,
and $b \in B(r)$ such that
$\ensuremath{\mathbf{A}} \ensuremath{\stackrel{.}{\cup} \neg .} U \not \models b$.
We make a case distinction: either $b$ is an ordinary literal or an external one.

If it is an ordinary default-negated atom $\naf c$,
then $\ensuremath{\mathbf{A}} \ensuremath{\stackrel{.}{\cup} \neg .} U \not\models b$ implies $\mathbf{T} c \in \ensuremath{\mathbf{A}}$
and $c \not\in U$, and therefore also $\ensuremath{\mathbf{A}} \ensuremath{\stackrel{.}{\cup} \neg .} Y \not\models b$.
So assume $b$ is an ordinary atom.
If $b \not \in U$ then $\ensuremath{\mathbf{A}} \not \models b$ and case (i) applies,
so assume $b \in U$.
Because $a \in H(r)$ and $b \in B(r)$,
we have $a \rightarrow b$ and therefore
either $a, b \in C$ or $a, b \in Y$ (because there are no ordinary
edges between $C$ and $Y$). But by assumption $a \in Y$, and
therefore $b \in Y$, hence $\ensuremath{\mathbf{A}} \ensuremath{\stackrel{.}{\cup} \neg .} Y \not \models b$.

If $b$ is an external literal, then there is no $q \in U$ with $a \rightarrow_e q$
and $q \not \in Y$. Otherwise, this would imply $q \in C$
and $C$ would have an incoming e-edge,
which contradicts the assumption that $C$ is a cut.
Hence, for all $q \in U$ with $a \rightarrow_e q$,
also $q \in Y$, and therefore the truth value of $b$ under
$\ensuremath{\mathbf{A}} \ensuremath{\stackrel{.}{\cup} \neg .} U$ and $\ensuremath{\mathbf{A}} \ensuremath{\stackrel{.}{\cup} \neg .} Y$ is the same.
Hence $\ensuremath{\mathbf{A}} \ensuremath{\stackrel{.}{\cup} \neg .} Y \not \models b$.

If (iii), then also
$\ensuremath{\mathbf{A}} \models h$ for some $h \in H(r) \setminus Y$ because $Y \subseteq U$
and therefore $H(r) \setminus Y \supseteq H(r) \setminus U$.
\hfill$\Box$
\end{proofsketch}

Next we prove, intuitively, that for each unfounded set $U$
of $\ensuremath{\Pi}$,
either the input to some external atom is unfounded itself, or $U$ is already detected
when $\ensuremath{\hat{\Pi}}$ is evaluated.
\begin{lemma}[EA-Input Unfoundedness]
\label{lemma:inputunfoundedness}
Let $U$ be an unfounded set of $\ensuremath{\Pi}$ wrt.~$\ensuremath{\mathbf{A}}$.
If there are no $x, y \in U$ such that $x \rightarrow_e y$,
then $U$ is an unfounded set of $\ensuremath{\hat{\Pi}}$ wrt.~$\ensuremath{\hat{\mathbf{A}}}$.
\end{lemma}
\begin{proofsketch}
If $U = \emptyset$, then the result holds trivially.
Otherwise, let $\hat{r} \in \ensuremath{\hat{\Pi}}$ such that $H(\hat{r}) \cap U \not= \emptyset$.
Let $a \in H(\hat{r}) \cap U$.
Observe that $\hat{r}$ cannot be an external atom guessing rule because
$U$ contains only ordinary atoms.
We show that one of the conditions
in Definition~\ref{def:unfoundedset}
holds for $\hat{r}$ wrt.~$\ensuremath{\hat{\mathbf{A}}}$.

Because $\hat{r}$ is no external atom guessing rule,
there is a corresponding rule $r \in \ensuremath{\Pi}$
containing external atoms in place of replacement atoms. Because $U$
is an unfounded set of $\ensuremath{\Pi}$ and $H(r) = H(\hat{r})$, either:
\begin{compactenum}[(i)]
\item $\ensuremath{\mathbf{A}} \not \models b$ for some $b \in B(r)$; or
\item $\ensuremath{\mathbf{A}} \ensuremath{\stackrel{.}{\cup} \neg .} U \not \models b$ for some $b \in B(r)$; or
\item $\ensuremath{\mathbf{A}} \models h$ for some $h \in H(r) \setminus U$
\end{compactenum}
If (i), let $b \in B(r)$ such that $\ensuremath{\mathbf{A}} \not \models b$
and $\hat{b}$ the corresponding literal in $B(\hat{b})$
(which is the same if $b$ is ordinary and the corresponding replacement
literal if $b$ is external). Then
also $\ensuremath{\hat{\mathbf{A}}} \not \models \hat{b}$ because $\ensuremath{\hat{\mathbf{A}}}$ is compatible.

For (ii), we make a case distinction: either $b$ is ordinary or external.

If $b$ is ordinary, then $b \in B(\hat{r})$ and $\ensuremath{\hat{\mathbf{A}}} \ensuremath{\stackrel{.}{\cup} \neg .} U \not \models b$
holds because $\ensuremath{\mathbf{A}}$ and $\ensuremath{\hat{\mathbf{A}}}$ are equivalent for ordinary atoms.

If $b$ is an external atom or default-negated external atom, then
no atom $p(\vec{c}) \in U$ is input to it, i.e. $p$ is
not a predicate input parameter of $b$; otherwise
we had $a \rightarrow_e p(\vec{c})$, contradicting our assumption
that $U$ has no internal e-edges.
But then $\ensuremath{\mathbf{A}} \ensuremath{\stackrel{.}{\cup} \neg .} U$ implies $\ensuremath{\mathbf{A}} \not \models b$
because the truth value of $b$ under $\ensuremath{\mathbf{A}} \ensuremath{\stackrel{.}{\cup} \neg .} U$
and $\ensuremath{\mathbf{A}}$ is the same. Therefore we can apply case (i).

If (iii), then also $\ensuremath{\hat{\mathbf{A}}} \models h$ for some $h \in H(\hat{r}) \setminus U$
because $H(r) = H(\hat{r})$ contains only ordinary atoms
and $\ensuremath{\mathbf{A}}$ is equivalent to $\ensuremath{\hat{\mathbf{A}}}$
for ordinary atoms.
\hfill$\Box$
\end{proofsketch}
\begin{example}
\label{ex:eaunfoundedness}
Reconsider the program $\ensuremath{\Pi}$ from Example~\ref{ex:cut}.
Then the unfounded set $U' = \{p,q\}$ wrt.~$\ensuremath{\mathbf{A}}' = \{\mathbf{T} p, \mathbf{T} q, \mathbf{F} r\}$
is already detected when $\ensuremath{\hat{\Pi}}$ consisting of
\begin{align*}
 e_{\amp{\mathit{id}}[r]}() \vee \mathit{ne}_{\amp{\mathit{id}}[r]}() &\leftarrow\\
 r &\leftarrow e_{\amp{\mathit{id}}[r]}()\\
 p &\leftarrow e_{\amp{\mathit{id}}[r]}()\\
 p &\leftarrow q\\
 q &\leftarrow p
\end{align*}
is evaluated by the ordinary ASP solver because $p \not\rightarrow_e q$ and $q \not\rightarrow_e p$.
In contrast, the unfounded set $U'' = \{p,q,r\}$ wrt.~$\ensuremath{\mathbf{A}}'' = \{\mathbf{T} p, \mathbf{T} q, \mathbf{T} r\}$
is \emph{not} detected by the ordinary ASP solver because $p,r \in U''$ and $p \rightarrow_e r$.
\end{example}

The essential property of unfounded sets of $\ensuremath{\Pi}$ wrt.~$\ensuremath{\mathbf{A}}$ that are not recognized
during the evaluation of $\ensuremath{\hat{\Pi}}$, is the existence of
cyclic dependencies including input atoms of some external atom.
Towards a formal characterization of a class of programs without this property, i.e.,
that do not require additional UFS checks, we define cycles as follows.
\begin{definition}[Cycle]
\label{def:cycle}
A \emph{cycle} under a binary relation $\circ$ is a sequence of elements $C = c_0, c_1, \ldots, c_n, c_{n+1}$
with $n \ge 0$,
such that $(c_i, c_{i+1}) \in \circ$ for all $0 \le i \le n$ and $c_0 = c_{n+1}$.
We say that a set $S$ \emph{contains a cycle} under $\circ$, if
there is a cycle $C = $ $c_0, c_1, \ldots, c_n, c_{n+1}$ under $\circ$ such that $c_i \in S$ for all $0 \le i \le n+1$.
\end{definition}

The following proposition states, intuitively, that each unfounded set
$U$ of $\ensuremath{\Pi}$ wrt.~$\ensuremath{\mathbf{A}}$
which contains no cycle through the input atoms to some external atom
has a corresponding unfounded set $U'$ of $\ensuremath{\hat{\Pi}}$ wrt.~$\ensuremath{\hat{\mathbf{A}}}$.
That is, the unfoundedness is already detected when $\ensuremath{\hat{\Pi}}$ is evaluated.

Let $\rightarrow^{d} \;=\; \rightarrow \cup \leftarrow \cup \rightarrow_e$,
where $\leftarrow$ is the inverse of $\rightarrow$, i.e. $\leftarrow
\;=\; \{ (x,y) \mid (y,x) \in\; \rightarrow \}$.
A cycle $c_0, c_1, \ldots, c_n, c_{n+1}$ under $\rightarrow^{d}$
is called an \emph{e-cycle}, iff it contains e-edges, i.e.,
iff $(c_i, c_{i+1}) \in \rightarrow_e$ for some $0 \le i \le n$.
\begin{proposition}[Relevance of e-cycles]
\label{prop:ecyclerelevance}
Let $U \not= \emptyset$ be an unfounded set of $\ensuremath{\Pi}$ wrt.~$\ensuremath{\mathbf{A}}$
that does not contain any e-cycle under $\rightarrow^{d}$.
Then, there exists a nonempty unfounded set of $\ensuremath{\hat{\Pi}}$ wrt.~$\ensuremath{\hat{\mathbf{A}}}$.
\end{proposition}
\begin{proofsketch}
We define the \emph{reachable set} $R(a)$ from some atom $a$ as
$$R(a) = \{ b \mid (a,b) \in \{\rightarrow \cup \leftarrow\}^{*} \},$$
i.e. the set of atoms $b \in U$ reachable from $a$ using edges from $\rightarrow \cup \leftarrow$ only but no e-edges.

We first assume that $U$ contains at least one e-edge, i.e. there are $x, y \in U$ such that $x \rightarrow_e y$.
Now we show that there is a $u \in U$ with outgoing e-edge (i.e. $u \rightarrow_e v$ for some $v \in U$),
but such that $R(u)$ has no incoming e-edges (i.e.
for all $v \in R(u)$ and $b \in U$, $b \not \rightarrow_e v$ holds).
Suppose to the contrary that for all $a$ with outgoing e-edges,
the reachable set $R(a)$ has an incoming e-edge.
We now construct an e-cycle
under $\rightarrow^{d}$,
which contradicts our assumption.
Start with an arbitrary node with an outgoing e-edge $c_0 \in U$ and let $p_0$
be the (possibly empty) path (under $\rightarrow \cup \leftarrow$) from $c_0$ to the node
$d_0 \in R(c_0)$ such that $d_0$ has an incoming e-edge, i.e. there is a $c_1$ such that $c_1 \rightarrow_e d_0$;
note that $c_1 \not \in R(c_0)$\footnote{
Whenever $x \rightarrow_e y$ for $x, y \in U$,
then there is no path from $x$ to $y$ under $\rightarrow \cup \leftarrow$,
because otherwise we would have an e-cycle under $\rightarrow^{d}$.
}.
By assumption, also some node $d_1$ in $R(c_1)$ has an incoming e-edge (from some node $c_2 \not \in R(c_1)$). Let $p_1$ be the path from
$c_1$ to $d_1$, etc. By iteration we can construct the
concatenation of the paths $p_0, (d_0, c_1), p_1, (d_1, c_2), p_2, \ldots, p_i, (d_i, c_{i+1}), \ldots$,
where the $p_i$ from $c_i$ to $d_i$
are the paths within reachable sets, and the $(d_i, c_{i+1})$ are the e-edges between reachable sets.
However, as $U$ is finite some nodes on this path must be equal, i.e., a prefix of the
constructed sequence represents an e-cycle (in reverse order).

This proves that $u$ is a node with outgoing e-edge but such that $R(u)$ has no incoming e-edges.
We next show that $R(u)$ is a cut. Condition (i) is immediately satisfied
by definition of $u$. Condition (ii) is shown as follows.
Let $u' \in R(u)$ and $v' \in U \setminus R(u)$. We have to show that $u' \not \rightarrow v'$
and $v' \not \rightarrow u'$. Suppose, towards a contradiction, that $u' \rightarrow v'$.
Because of $u' \in R(u)$, there is a path from $u$ to $u'$ under $\rightarrow \cup \leftarrow$.
But if $u' \rightarrow v'$, then
there would also be a path from $u$ to $v'$ under $\rightarrow \cup \leftarrow$ and $v'$ would be in $R(u)$, a contradiction
Analogously, $v' \rightarrow u'$ would also imply that there is a path from $u$ to $v'$
because there is a path from $u$ to $u'$, again a contradiction.

Therefore, $R(u)$ is a cut of $U$, and by Lemma~\ref{lemma:ufsreduction}, it follows that $U \setminus R(u)$ is an unfounded set.
Observe that $U \setminus R(u)$ contains one e-edge less than $U$ because $u$ has an outgoing e-edge.
Further observe that $U \setminus R(u) \not= \emptyset$ because there is a $w \in U$
such that $u \rightarrow_e w$ but $w \not \in R(u)$.
By iterating this argument, the number of e-edges in the unfounded set can be reduced to zero in a
nonempty core.
Eventually, Lemma~\ref{lemma:inputunfoundedness} applies, proving that the remaining set
is an unfounded set of $\ensuremath{\hat{\Pi}}$.
\hfill$\Box$
\end{proofsketch}
\begin{corollary}
\label{cor:ecyclefreeprograms}
If there is no e-cycle under $\rightarrow^{d}$
and $\ensuremath{\hat{\Pi}}$ has no unfounded set wrt.~$\ensuremath{\hat{\mathbf{A}}}$, then~$\ensuremath{\mathbf{A}}$ is unfounded-free for $\ensuremath{\Pi}$.
\end{corollary}
\begin{proofsketch}
Suppose there is an unfounded set $U$ of $\ensuremath{\Pi}$ wrt.~$\ensuremath{\mathbf{A}}$.
Then it contains no e-cycle because there is no e-cycle under $\rightarrow^{d}$.
Then by Proposition~\ref{prop:ecyclerelevance} there is an unfounded set of $\ensuremath{\hat{\Pi}}$
wrt.~$\ensuremath{\hat{\mathbf{A}}}$, which contradicts our assumption.
\hfill$\Box$
\end{proofsketch}

This corollary can be used as follows to increase performance of an evaluation algorithm:
if there is no cycle under $\rightarrow^{d}$ containing e-edges,
then an explicit unfounded set check is not necessary
because the unfounded set check made during evaluation of~$\ensuremath{\hat{\Pi}}$
suffices.
Note that this test can be done efficiently (in fact in linear time, similar to
deciding stratifiability of an ordinary logic program).
Moreover, in practice one can abstract from
$\rightarrow^{d}$ by using analogous relations on the
level of predicate symbols instead of atoms. Clearly, if there is no e-cycle
in the predicate dependency graph,
then there can also be no e-cycle in the atom dependency graph.
Hence, the predicate dependency graph can be used to decide whether
the unfounded set check can be skipped.
\begin{example}
All example programs considered until here require an UFS check, but
the program $\ensuremath{\Pi} = \{ \mathit{out}(X) \leftarrow \ext{\mathit{diff}}{\mathit{set}_1, \mathit{set}_2}{X} \} \cup F$
does not for any set of facts $F$, because there is no e-cycle under $\rightarrow^{d}$,
where $\mathit{diff}$ computes the set difference of the extensions of $\mathit{set}_1$ and $\mathit{set}_2$.

Also $\ensuremath{\Pi} = \{ \mathit{str}(Z) \leftarrow \mathit{dom}(Z), \mathit{str}(X), \mathit{str}(Y), \naf \ext{\mathit{concat}}{X,Y}{Z} \}$
(where $\amp{\mathit{concat}}$ takes two constants and computes their string concatenation) does not need such a check;
there is a  cycle over an external atom, but no e-cycle under $\rightarrow^{d}$.
\end{example}

Moreover, the following proposition states that, intuitively, if $\ensuremath{\hat{\Pi}}$
has no unfounded sets wrt.~$\ensuremath{\hat{\mathbf{A}}}$, then
any unfounded set $U$ of $\ensuremath{\Pi}$ wrt.~$\ensuremath{\mathbf{A}}$ must contain
an atom which is involved in a cycle under $\rightarrow^{d}$ that has an e-edge.
\begin{definition}[Cyclic Input Atoms]
For a program $\ensuremath{\Pi}$, an atom $a$ is a \emph{cyclic input atom},
iff there is an atom $b$ such that $b \rightarrow_e a$ and there is
a path from $a$ to $b$ under $\rightarrow^{d}$.
\end{definition}

Let $\mathit{CA}(\ensuremath{\Pi})$ denote the set of
all cyclic input atoms of program $\ensuremath{\Pi}$.
\begin{proposition}[Unfoundedness of Cyclic Input Atom]
\label{prop:unfoundednesscyclicpredicateinput}
Let $U\neq\emptyset$ be an unfounded set of $\ensuremath{\Pi}$ wrt.~$\ensuremath{\mathbf{A}}$ such that
 $U$ does not contain cyclic input atoms.
Then, $\ensuremath{\hat{\Pi}}$ has a nonempty unfounded set wrt.~$\ensuremath{\hat{\mathbf{A}}}$.
\end{proposition}
\begin{proofsketch}
If $U$ contains no cyclic input atoms, then all
cycles under $\rightarrow^{d}$ containing e-edges
in the atom dependency graph of $\ensuremath{\Pi}$
are broken, i.e. $U$
does not contain an e-cycle under $\rightarrow^{d}$.
Then by Proposition~\ref{prop:ecyclerelevance}
there is an unfounded set of $\ensuremath{\hat{\Pi}}$ wrt.~$\ensuremath{\hat{\mathbf{A}}}$.
\hfill$\Box$
\end{proofsketch}

Proposition~\ref{prop:unfoundednesscyclicpredicateinput}
allows for generating the additional nogood
$\{ \mathbf{F} a \mid a \in \mathit{CA}(\ensuremath{\Pi}) \}$
and adding it to $\Gamma^{\ensuremath{\mathbf{A}}}_{\ensuremath{\Pi}}$.
Again, considering predicate symbols instead of atoms is possible
to reduce the overhead introduced by the dependency graph.

\section{Program Decomposition}

It turns out that the usefulness of the decision criterion can be increased
by decomposing the program into components, such that
the criterion can be applied component-wise. This allows for restricting
the unfounded set check to components with e-cycles,
whereas e-cycle-free components can be ignored in the check.

Let $\mathcal{C}$ be a partitioning of the ordinary atoms $A(\ensuremath{\Pi})$
of $\ensuremath{\Pi}$
into subset-maximal strongly connected components under $\rightarrow \cup \rightarrow_e$.
We define
for each partition $C \in \mathcal{C}$ the subprogram $\ensuremath{\Pi}_{C}$
\emph{associated with $C$} as
$\ensuremath{\Pi}_{C} = \{ r \in \ensuremath{\Pi} \mid H(r) \cap C \not= \emptyset \}$.

We next show that if a program %
has an unfounded set $U$ wrt.~$\ensuremath{\mathbf{A}}$,
 then $U\,{\cap}\,C$ is an unfounded set wrt.~$\ensuremath{\mathbf{A}}$ for the subprogram of some strongly
connected component $C$.
\begin{proposition}
\label{prop:programdecomposition}
Let $U \not= \emptyset$ be an unfounded set of $\ensuremath{\Pi}$ wrt.~$\ensuremath{\mathbf{A}}$.
Then, for some $\ensuremath{\Pi}_{C}$ with $C \in \mathcal{C}$ it holds
that $U \cap C$ is a nonempty unfounded set of $\ensuremath{\Pi}_{C}$ wrt.~$\ensuremath{\mathbf{A}}$.
\end{proposition}
\begin{proofsketch}
Let $U$ be a nonempty unfounded set of $\ensuremath{\Pi}$ wrt.~$\ensuremath{\mathbf{A}}$.
Because $\mathcal{C}$ is a decomposition of $A(\ensuremath{\Pi})$ into strongly
connected components, the \emph{component dependency graph}
$$\left\langle \mathcal{C},
\{ (C_1, C_2) \mid C_1, C_2 \in \mathcal{C}, \exists a_1 \in C_1, a_2 \in C_2:  (a_1, a_2) \in \rightarrow \cup \rightarrow_e \} \right\rangle$$
is acyclic.
Following the hierarchical component dependency graph from the
nodes without predecessor components downwards, we can find
a ``first'' component which has a nonempty intersection with $U$,
i.e., there exists a component $C \in \mathcal{C}$ such that
$C \cap U \not= \emptyset$ but $C' \cap U = \emptyset$ for all transitive
predecessor components $C'$ of $C$.

We show that $U \cap C$ is an unfounded set of $\ensuremath{\Pi}_{C}$ wrt.~$\ensuremath{\mathbf{A}}$.
Let $r \in \ensuremath{\Pi}_{C}$ be a rule such that $H(r) \cap (U \cap C) \not= \emptyset$.
We have to show that one of the conditions of Definition~\ref{def:unfoundedset}
holds for $r$ wrt.~$\ensuremath{\mathbf{A}}$ and $U \cap C$.

Because $U$ is an unfounded set of $\ensuremath{\Pi}$ wrt.~$\ensuremath{\mathbf{A}}$
and $H(r) \cap (U \cap C) \not= \emptyset$ implies $H(r) \cap U \not= \emptyset$, we know
that one of the conditions holds for $r$ wrt.~$\ensuremath{\mathbf{A}}$ and $U$.
If this is condition (i) or (iii), then it trivially holds also wrt.~$\ensuremath{\mathbf{A}}$
and $U \cap C$ because these conditions depend only on the assignment $\ensuremath{\mathbf{A}}$, but not on
the unfounded set $U$.

If it is condition (ii), then $\ensuremath{\mathbf{A}} \ensuremath{\stackrel{.}{\cup} \neg .} U \not\models b$
for some (ordinary or external) body literal $b \in B(r)$.
We show next that the truth value of all literals in
$B(r)$ is the same under $\ensuremath{\mathbf{A}} \ensuremath{\stackrel{.}{\cup} \neg .} U$ and $\ensuremath{\mathbf{A}} \ensuremath{\stackrel{.}{\cup} \neg .}  (U \cap C)$,
which proves that condition (ii) holds also wrt.~$\ensuremath{\mathbf{A}}$ and~$U \cap C$.

If $b = \naf a$ for some atom $a$, then $\mathbf{T} a \in \ensuremath{\mathbf{A}}$ and $a \not\in U$
and consequently $a \not\in U \cap C$, hence $\ensuremath{\mathbf{A}} \ensuremath{\stackrel{.}{\cup} \neg .} (U \cap C) \not\models b$.
If $b$ is an ordinary atom, then either $\mathbf{F} b \in \ensuremath{\mathbf{A}}$,
which implies immediatly that $\ensuremath{\mathbf{A}} \ensuremath{\stackrel{.}{\cup} \neg .} (U \cap C) \not\models b$,
or $b \in U$. But in the latter case $b$ is either
in a predecessor component $C'$ of $C$ or in $C$ itself
(since $h \rightarrow b$ for all $h \in H(r)$).
But since $U \cap C' = \emptyset$
for all predecessor components of $C$, we know $b \in C$ and therefore $b \in (U \cap C)$,
which implies $\ensuremath{\mathbf{A}} \ensuremath{\stackrel{.}{\cup} \neg .} (U \cap C) \not\models b$.

If $b$ is a positive or default-negated external atom,
then all input atoms $a$ to $b$ are either
in a predecessor component $C'$ of $C$ or in $C$ itself
(since $h \rightarrow_e a$ for all $h \in H(r)$).
We show with a similar argument as before that the truth value of each
input atom $a$ is the same under $\ensuremath{\mathbf{A}} \ensuremath{\stackrel{.}{\cup} \neg .} U$
and $\ensuremath{\mathbf{A}} \ensuremath{\stackrel{.}{\cup} \neg .} (U \cap C)$:
if $\ensuremath{\mathbf{A}} \ensuremath{\stackrel{.}{\cup} \neg .} U \models a$, then $\mathbf{T} a \in \ensuremath{\mathbf{A}}$
and $a \not\in U$, hence $a \not\in (U \cap C)$ and
therefore $\ensuremath{\mathbf{A}} \ensuremath{\stackrel{.}{\cup} \neg .} (U \cap C) \models a$.
If $\ensuremath{\mathbf{A}} \ensuremath{\stackrel{.}{\cup} \neg .} U \not\models a$, then either
$\mathbf{F} a \in \ensuremath{\mathbf{A}}$, which immediately implies
$\ensuremath{\mathbf{A}} \ensuremath{\stackrel{.}{\cup} \neg .} (U \cap C) \not\models a$,
or $a \in U$.
But in the latter case $a$ must be in $C$ because $U \cap C' = \emptyset$
for all predecessor components $C'$ of $C$. Therefore $a \in (U \cap C)$
and consequently $\ensuremath{\mathbf{A}} \ensuremath{\stackrel{.}{\cup} \neg .} (U \cap C) \not\models a$.
Because all input atoms $a$ have the same truth value under
$\ensuremath{\mathbf{A}} \ensuremath{\stackrel{.}{\cup} \neg .} U$ and $\ensuremath{\mathbf{A}} \ensuremath{\stackrel{.}{\cup} \neg .} (U \cap C)$,
the same holds also for the positive or default-negated external atom $b$
itself.
\hfill $\Box$
\end{proofsketch}

This proposition states that a search for unfounded sets can be done
independently for the subprograms $\ensuremath{\Pi}_{C}$
for all $C \in \mathcal{C}$.
If there exists a global unfounded set, then there exists also one
in at least one of the program components.
However, we know by Corollary~\ref{cor:ecyclefreeprograms} that
programs $\ensuremath{\Pi}$ without e-cycles cannot contain unfounded sets, which are not
already detected when $\ensuremath{\hat{\Pi}}$ is solved. If we apply this proposition
to the subprograms $\ensuremath{\Pi}_{C}$, we can safely ignore e-cycle-free
program components.
\begin{example}
Reconsider the program $\ensuremath{\Pi}$ from Example~\ref{ex:cut}.
Then $\mathcal{C}$ contains the components $C_1 = \{p,q\}$
and $C_2 = \{r\}$ and we have
$\ensuremath{\Pi}_{C_1} = \{ p \leftarrow \amp{\mathit{id}[r]}(); p \leftarrow q; q \leftarrow p \}$
and
$\ensuremath{\Pi}_{C_2} = \{ r \leftarrow \amp{\mathit{id}[r]}() \}$.
By Proposition~\ref{prop:programdecomposition}, each unfounded set
of $\ensuremath{\Pi}$ wrt.~some assignment can also detected over one of the components.
Consider e.g. $U = \{p,q,r\}$ wrt.~$\ensuremath{\mathbf{A}} = \{ \mathbf{T} p, \mathbf{T} q, \mathbf{T} r\}$.
Then $U \cap \{r\} = \{r\}$ is also an unfounded set of $\ensuremath{\Pi}_{C_2}$ wrt.~$\ensuremath{\mathbf{A}}$.

By separate application of Corollary~\ref{cor:ecyclefreeprograms} to the
components, we can conclude that there can be no unfounded sets over $\ensuremath{\Pi}_{C_1}$
that are not already detected when $\ensuremath{\hat{\Pi}}$ is evaluated (because it has no e-cycles).
Hence, the additional unfounded set check is only necessary for $\ensuremath{\Pi}_{C_2}$.
Indeed, the only unfounded set which is not detected when $\ensuremath{\hat{\Pi}}$ is
evaluated is $\{r\}$ of $\ensuremath{\Pi}_{C_2}$ wrt.~any interpretation $\ensuremath{\mathbf{A}} \supseteq \{\mathbf{T} r\}$.
\end{example}

Finally, one can also show that splitting, i.e., the component-wise check for foundedness,
does not lead to spurious unfounded sets.
\begin{proposition}
If $U$ is an unfounded set of $\ensuremath{\Pi}_{C}$
wrt.~$\ensuremath{\mathbf{A}}$ such that $U \subseteq C$, then $U$
is  an unfounded set of $\ensuremath{\Pi}$ wrt.~$\ensuremath{\mathbf{A}}$.
\end{proposition}
\begin{proofsketch}
If $U = \emptyset$, then the result holds trivially.
By definition of $\ensuremath{\Pi}_{C}$ we have $H(r) \cap C = \emptyset$ for all
$r \in \ensuremath{\Pi} \setminus \ensuremath{\Pi}_{C}$.
By precondition of the proposition we have $U \subseteq C$.
But then $H(r) \cap U = \emptyset$ for all $r \in \ensuremath{\Pi} \setminus \ensuremath{\Pi}_{C}$
and $U$ is an unfounded set of $\ensuremath{\Pi}$ wrt.~$\ensuremath{\mathbf{A}}$.
\hfill $\Box$
\end{proofsketch}

\nop{
\section{Unfounded Set Check over Partial Interpretations}
\label{sec:partialinterpretations}

In some cases a detected unfounded set wrt.~a partial interpretation
implies the existence of an unfounded set wrt.~any completion of
the interpretation.
Clearly, a search for unfounded sets over incomplete interpretations
is only useful if we can be sure that detected unfounded sets
will remain unfounded for arbitrary completions of the interpretations.

Formally, we can show the following:

\begin{proposition}
Let $\ensuremath{\Pi}'$ be a program, $\ensuremath{\mathbf{A}}'$ be a complete interpretation
(on $\ensuremath{\Pi}'$)
and $U$ be an unfounded set of $\ensuremath{\Pi}'$ wrt.~$\ensuremath{\mathbf{A}}'$.
If $\ensuremath{\Pi} \supseteq \ensuremath{\Pi}'$ such that $U \cap H(r) = \emptyset$
for all $r \in \ensuremath{\Pi} \setminus \ensuremath{\Pi}'$, then
$U$ is an unfounded set of $\ensuremath{\Pi}$ wrt.~any $\ensuremath{\mathbf{A}} \supseteq \ensuremath{\mathbf{A}}'$.
\end{proposition}

Intuitively, the proposition states that an unfounded set
of a program wrt.~some interpretation will remain an unfounded set
if the program is extended by rules which do not derive any of
the elements in the unfounded set.

\begin{proofsketch}
Let $\ensuremath{\Pi}'$ be a program, $\ensuremath{\mathbf{A}}'$ be a complete interpretation
(on $\ensuremath{\Pi}'$)
and $U$ be an unfounded set of $\ensuremath{\Pi}'$ wrt.~$\ensuremath{\mathbf{A}}'$.
Further let $\ensuremath{\Pi} \supseteq \ensuremath{\Pi}'$ and $\ensuremath{\mathbf{A}} \supseteq \ensuremath{\mathbf{A}}'$.

We have to show that if $U \cap H(r) \not= \emptyset$, then one of
the conditions in Definition~\ref{def:unfoundedset} holds for some all $r \in \ensuremath{\Pi}$
wrt.~$\ensuremath{\mathbf{A}}$ and $U$.
Let $r \in \ensuremath{\Pi}$. If $r \in \ensuremath{\Pi}'$, then one of the conditions holds
because $U$ is an unfounded set of $\ensuremath{\Pi}'$ wrt.~$\ensuremath{\mathbf{A}}'$
and $\ensuremath{\mathbf{A}}'$ is complete on $\ensuremath{\Pi}'$.
If $r \not \in \ensuremath{\Pi}'$, then $U \cap H(r) = \emptyset$ by assumption.
\hfill$\Box$.
\end{proofsketch}

\begin{corollary}
If some assignment $\ensuremath{\mathbf{A}}'$ is complete on
a subprogram $\ensuremath{\Pi}' \subseteq \ensuremath{\Pi}$
and $\ensuremath{\Pi}'$ has an unfounded set $U$ wrt.~$\ensuremath{\mathbf{A}}'$
such that $U \cap H(r) = \emptyset$ for all $r \in \ensuremath{\Pi} \setminus \ensuremath{\Pi}'$,
then no $\ensuremath{\mathbf{A}} \supseteq \ensuremath{\mathbf{A}}'$ is an answer-set of $\ensuremath{\Pi}$.
\end{corollary}

This result can be used as follows. For a partial interpretation $\ensuremath{\mathbf{A}}'$
which is complete on a subprogram $\ensuremath{\Pi}' \subseteq \ensuremath{\Pi}$, if
$\Gamma^{\ensuremath{\mathbf{A}}'}_{\ensuremath{\Pi}'} \cup \{ \{ \mathbf{F} a \} \mid r \in \ensuremath{\Pi} \setminus \ensuremath{\Pi}', a \in H(r)  \}$
has a solution, then no completion of $\ensuremath{\mathbf{A}}'$ can be an answer set
of $\ensuremath{\Pi}$.

\begin{example}
\label{ex:manyufs3}
Consider again the program $\ensuremath{\Pi}$
from Examples~\ref{ex:manyufs} and~\ref{ex:manyufs2}
and suppose we have the partial
interpretation $\ensuremath{\mathbf{A}}' = \{p\}$, i.e., the guess
over the $x_i$ for $1 \le i \le n$ was not done yet.
Nevertheless, we can already make an unfounded set check
over the partial program $\ensuremath{\Pi}' = \{ p \leftarrow \ext{\mathit{id}}{p}{} \}$
because $\ensuremath{\mathbf{A}}'$ is complete over this program.
The detected unfounded set $U = \{ p \}$ does not intersect with
the head of a rule $r \in \ensuremath{\Pi} \setminus \ensuremath{\Pi}' = \{ x_1 \vee x_2 \vee \ldots x_n \leftarrow \}$.
Therefore we can be sure that $U$ is also an unfounded set of $\ensuremath{\Pi}$ wrt.~arbitrary
completions of $\ensuremath{\mathbf{A}}'$ and we can immediatly backtrack, e.g.
by learning $L_2(U,\ensuremath{\mathbf{A}}',\ensuremath{\Pi}')$.
\end{example}
}

\section{Implementation and Evaluation}
\label{sec:implementation}

\myfigureargu{tb}

For implementing our technique,
we integrated \clasp{} into our prototype system \dlvhex{};
we use \clasp{} as an ASP solver for computing compatible sets
and as a SAT solver for solving the nogood set of the UFS check.
We evaluated the implementation
on a Linux server with two 12-core AMD 6176 SE CPUs with 128GB RAM.

\leanparagraph{Argumentation Benchmarks}
In this benchmark we compute
ideal set extensions for randomized instances
of abstract argumentation frameworks~\cite{dung1995-aij}
of different sizes.
In these instances, the cycles involve usually
only small parts of the overall programs, hence
the program decomposition is very effective.
Table~\ref{fig:argumentation} shows results of our experimental evaluation
on argumentation benchmark instances;
for computing average times, we considered 300 seconds for instances that timed out.
The encodings contain a cyclic part with cycles over external atoms,
and a cyclic part with cycles that do not contain external atoms.
Therefore in these instances our new approach can help in limiting the set of atoms
for which unfounded sets must be checked,
which explains the significant performance gain
due to less time spent in the UFS check.

\leanparagraph{Multi-Context System Benchmarks}
MCSs~\cite{be2007} are a formalism for interlinking knowledge based systems;
in~\cite{efsw2010-kr}, \emph{inconsistency explanations (IEs)}\/ for an MCS
were defined.
This benchmark
computes the IEs, which correspond 1-1 to answer sets of an encoding
rich in cycles through external atoms
(which evaluate local knowledge base semantics).
We use random instances of different topologies
created with an available benchmark generator.
For the MCS benchmarks we tested 68 consistent and 88 inconsistent
MCSs for which we compute inconsistency explanations~\cite{efsw2010-kr}.
This encoding contains saturation over external atoms,
where nearly all cycles in the \hex{}-program
contain at least one external atom.
Therefore the methods we introduce in this work
can only very rarely reduce the set of atoms
for which the UFS check needs to be performed.

The benchmark result for MCS instances
confirms that the syntactic check we introduce in this paper
is very cheap and does not impede %
performance,
even if an instance does not admit a considerable simplification for
the UFS check:
over all 156 instances,
we had an overall runtime of 25357 seconds
with the standard approach,
and a runtime of 25115 seconds with our new approach;
the gain is 242 seconds which is less than one percent speedup
(for enumerating all inconsistency explanations) by applying our method.
This is a very small gain,
and there is no difference in the number of instances that timed out.

\leanparagraph{Default Reasoning over Description Logics Benchmarks}
Another application of \hex-programs is the
DL-plugin~\cite{eiks2009-amai}, which integrates description logics
ontologies with rules. This allows, for instance, default reasoning over description
logic knowledge bases, which is not possible in DL knowledge bases alone.
Defaults require cyclic dependencies over external atoms.
However, as all such dependencies involve default negated atoms,
we have no cycles according to Definition~\ref{def:atomdependency},
which respects only positive dependencies. Hence, the decision criterion
comes to the conclusion that no UFS check is required.

We used variants of the benchmarks presented in~\cite{efkr2012-tplp},
which query wines from an ontology and
classify them as red or white wines, where a wine is assumed to be white
unless the ontology explicitly entails %
the contrary.
In this scenario, the
decision criterion eliminates all unfounded set checks. However,
as there is only one compatible set per instance, there would be only one
unfounded set check anyway, hence the speedup due to the decision criterion
is not significant.
But the effect of the decision criterion
can be increased by slightly modifying the scenario such that there
are multiple compatible sets. This can be done, for instance, by
nondeterministic default classifications, e.g., if a wine is not
Italian, then it is either French or Spanish by default.
Our experiments have shown that with a small number of compatible sets,
the performance enhancement due to the decision criterion is marginal,
but increases with larger numbers of compatible sets. For instance,
for $243$ compatible sets (and thus $243$ unfounded set checks)
we could observe a speedup from $13.59$ to $12.19$
seconds.

\section{Conclusion}
\label{sec:conclusion}

The evaluation of \hex-programs requires a minimality check of model
candidates which is realized as an equivalent search for unfounded sets (UFS).
However, this check is computationally costly. Moreover, during construction
of the model candidate, the ASP solver used as a backend has already performed
a ``restricted'' form of unfounded set check, i.e., an UFS check over
the program $\ensuremath{\hat{\Pi}}$, viewing external atoms as ordinary ones. Hence,
it already excludes certain unfounded candidates. Redoing a complete UFS
search is thus a waste of resources, and the goal is to
minimize the number of additional foundedness checks.

In this paper we presented a syntactic criterion which can be
efficiently tested and allows to decide whether an additional UFS check
is necessary for a given program. It turned out
that %
the essential property is the existence of cyclic dependencies of atoms
which involve predicate inputs to external atoms. If no such
dependencies exist, then there is no need for an additional check, and
the check built into the ordinary ASP solver is already sufficient. In
further elaboration, we have refined the basic idea by splitting the
input program into components. This allows for independent applications
of the decision criterion to the different components. Thus, the UFS
check is restricted to relevant parts of the program, while it can
safely be ignored for other parts.

Related to our work is~\cite{Drescher08conflict-drivendisjunctive}, where
a similar program decomposition is used, yet
for ordinary programs only. While we consider e-cycles, which are specific
for \hex-programs,
the interest in \cite{Drescher08conflict-drivendisjunctive} is with head-cycles
with respect to disjunctive rule heads. In fact, our implementation
may be regarded as an extension of the work in~\cite{Drescher08conflict-drivendisjunctive},
since the evaluation of $\ensuremath{\hat{\Pi}}$ follows their principles of performing UFS checks
in case of head-cycles.
Note however, that the applied component splitting %
does not generalize the well-known splitting theorem~\cite{lif94}
as we consider only positive dependencies for ordinary atoms.

An interesting issue for further research is to consider refinements
of the decision criterion, or alternative criteria. One direction for
refinement is to dynamically take the model candidate into account, in
addition to the program structure, which intuitively may prune
dependencies and thus allow to skip the UFS check even in the presence
of (syntactic) e-cycles. Another extension is to exploit additional
semantic information on the external atoms, e.g., such as
(anti-)monotonicity etc. Moreover, a more extensive experimental
analysis is subject of our future work, where case studies may give rise to
to alternative criteria and further optimizations.

\ifinlineref
\input{references}
\else
\bibliographystyle{splncs03}

redpajama_set_name: RedPajamaArXiv


Let the animal print obsession continue, this one is our new favorite! Dark brown and taupe colored zebra stripes shape this top featuring a high neckline that ties in the back and a chic swing shape. We can't get enough of this bold print and love it paired with a pop of teal or pink! Model is 5'8'' and wearing a size small.


Autism is a condition that is becoming increasingly common. Our Autism ID Cards help provide valuable and potentially lifesaving information. If you are autistic or have an autistic loved one, then this card should be carried at all times. The card can be customized as you wish. Our standard card includes a photo, name, emergency contact, and medications needed.


text:
Home Western Classical Musicians Look Eastward for Inspiration in the Dayton Philharmonic Masterworks...
Western Classical Musicians Look Eastward for Inspiration in the Dayton Philharmonic Masterworks Concert East Meets West
DAYTON, OH (December 16, 2021) – On Friday, January 7, 2022 and Saturday, January 8, 2022 at 8:00 pm in the Mead Theatre of the Schuster Center, Artistic Director and Conductor Neal Gittleman and the Dayton Philharmonic Orchestra (DPO) continue the Dayton Performing Arts Alliance's 2021‒2022 Season with a Masterworks concert entitled, East Meets West.
The Louis S. Cantor, Rose Sorokin Cantor, Samuel L. Cantor, and Lena Cantor Endowed Artist for this concert is DPO Principal Clarinet John Kurokawa
This evening of East Meets West opens with Charles Tomlinson Griffes's tone poem "The Pleasure Dome of Kubla Khan," inspired by the unfinished poem by English romantic poet Samuel Taylor Coleridge. The work, which came to Griffes in a dream, evokes images taken from Coleridge's poetic images of a "sunny dome" and "caves of ice."
While many composers of Western classical music have looked to exotic lands for inspiration, Reena Esmail's Indian musical roots let her look West and East for her compositions. Esmail says of her Clarinet Concerto, "Hindustani music is an aural tradition: the nuance of a phrase is picked up through call and response, by hearing and repeating. In both movements of this concerto, the melodies that start in the clarinet eventually find their way into the orchestra. The aural transfer of these melodies to the western musicians is embedded in the piece itself, and the exchange of musical cultures is taking place in real time, before your ears." Dayton Philharmonic Principal Clarinet John Kurokawa takes the spotlight for this haunting and exhilarating work.
For 150 years in the 16th and 17th centuries, Vienna was the nexus of East-West interactions due to the two Turkish sieges of the city, which, led (once the danger was over) to a Viennese fascination with all things Turkish. After his move from his birthplace of Salzburg to Vienna, Mozart pulled from this Turkish influence, using a Turkish harem as the setting for his first big-hit opera, The Abduction from the Seraglio. The opera's overture features the jingling sounds of Turkish percussion instruments and evokes the noise the Turkish army bands made outside the city gates during the sieges.
Strauss's beautiful Suite from Der Rosenkavalier crowns this enchanting Masterworks concert, with ravishing melodies and seductive waltzes that transport audiences to Vienna's opulent golden age.
The DPAA is excited to welcome audiences back to the 2021–2022 Season. The health and safety of patrons, performers, staff, and volunteers is our top priority. Beginning November 22, 2021, in partnership with DPAA's venue partner Dayton Live, the following new health and safety protocols will be in place at all performances and events until further notice:
Tickets for East Meets West start at $5 and are available at the box office by calling (937) 228-3630 or online at www.daytonperformingarts.org. The $5 Tickets are sponsored by AES Ohio as part of DPAA's "The Arts Are for Everyone" program. Senior, teacher and student discounts are available at the box office. For more information or to order subscriptions, including flexible subscription types that include performances by Dayton Philharmonic, Dayton Opera and Dayton Ballet, visit www.daytonperformingarts.org.

redpajama_set_name: RedPajamaCommonCrawl


for use in emergencies, as well as for various kinds of humanitarian assistance.
and international NGOs and a variety of UN agencies.
250 beds (NorHosp). Products include mobile module-based field hospitals, clinical units, backpacks, hospital beds and stretcher systems.
we also have long experience customizing solutions for specific needs.
was founded in 1913 with the purpose of trading in pharmaceutical products, drugs and chemicals in competition with foreign wholesalers.
of medicines and in 1956, the Norwegian Parliament decided that the wholesale supply of medicines in Norway was to be taken over by the government, represented by Norsk Medisinaldepot (NMD).
Mediq Norge then became a supplier of medical equipment and consumables to pharmacies, hospitals and other health institutions.
We are now the largest supplier of these products in Norway.
Mediq Norge complies with the official standards of NS-EN ISO.
Mediq Norge is part of «The Norwegian Emergency Preparedness System» (NOREPS). NOREPS contributes to the efforts of UN agencies and NGOs to rapidly provide both supplies and personnel to areas of disaster. Supplies can be airborne in less than 24 hours, and teams of relief workers can be operable in the field within 72 hours.
The NGOs and the Norwegian Ministry of Foreign Affairs are our partners in the administration of NOREPS, and may provide further information upon its use and funding.
Mediq Norway has preparedness storage and services for Norwegian Authorities, Red Cross and UN agencies.


Students can access practice sets online to learn basics of their subject in a simple to understand manner. They help students to get direct practical experience in basic components in a field of study such as accounting.
At times tutors assign several Perdisco practice sets, and it becomes a challenge for students to complete and solve them within given deadline. Ukassignmentclub.co.uk offers the most exceptional Perdisco practice set help to students who are unable to complete due to lack of time or skill. You should not suffer the effects of failing to complete Perdisco assignment service when we have the time and experts to help you. Contact us or visit our order page and you are on your way to accessing expert help.
Assignmentclub.co.uk is a leading Perdisco practice set providers since we use a highly talented experienced team that works to dedicated to help the students achieve their goals. We deliver our promises as we have the mastery and experience on the right way of working on Perdisco questions to reach accurate answers. Our experts have solved thousands of Perdisco practice sets, and they know the right way to customize them per the needs.
We customize Perdisco modules according to specific needs of our clients. It is the reason we have experienced tutors who know the best solutions to get the correct answers and deliver a high percentage of all customers. They are thorough in their work, and a large number of satisfied customers are the proof that we have been achieving the score and results that students require from us. Customer satisfaction from achieving the desired results is the reason why UK Assignment Club is one of the top platforms in offering help with Perdisco practice sets.
We will match you with an expert who has extensive knowledge on the way to work out solutions for Perdisco practice sets. You will get a specialist with a masters or PhD degree in your academic area and experience in writing assignments similar to your topic. The specialist is dedicated to helping you achieve best grades and will take time to understand the question, complete within a short time and revise to ensure accuracy before delivery.
You can access our service at any location and time if you have a computer or a gadget with an internet connection. You can reach our customer support representatives for inquiries on Perdisco practice set help by live chat, email, phone call or social media platforms. We have simplified the process further by providing an online order system that allows you to fill order specifications and get an instant quote. If you make payment, we will soon assign your Perdisco practice sets to someone from your field to complete within the given time.
Assignmentclub.co.uk understands the value of time for Perdisco practice sets and the impact of lateness on grades or delaying other tasks. We do the best to ensure that our practice sets help is complete before your deadline. We use experienced professionals who can complete the test fast within the required time while maintaining high levels of accuracy.
The costs of our service are reasonable because we want to help you and many other students to get the top grade for their Perdisco tests. We keep our prices to an affordable level as possible. We achieve an excellent score on the first attempt, but in the case of a low grade, another expert will request and solve another set of questions at no extra cost.
I thank you for help with my Perdisco practice sets within a short time. I appreciate your role in my grades.
I like the quality of Perdisco practice set help. You helped me to get an excellent grade, and the price is fantastic.
I recommend assignmentclub.co.uk to students who use Perdisco practice sets to improve their knowledge. You will get a specialist in your topic to complete the practice set and explain the solutions.
. Ellen G. Indiana, USA.


text:
California Dead Last Among U.S. States In 'Quality Of Life,' Study Finds
By Joseph Curl
Mar 1, 2018 DailyWire.com
California ranks 50th (out of 50, not 57 as former President Barack Obama once said) among U.S. states in quality of life, according to a new study by U.S. News & World Report.
That's right, California ranks lower than New Jersey (49th) and Alaska (which actually comes in at a respectable 19th).
"The ignominious honor reflects California's low marks in the sub-categories of environmental quality and social engagement. The latter category measures voting participation and community bonds," U.S. News wrote.
"Californians scored poorly in part because they're simply insufferable, U.S. News suggested." Boy, that's an understatement.
"In addition to a healthy environment, a person's quality of life is largely a result of their interactions with those around them," the magazine wrote in a blurb accompanying the results.
One way to measure quality life is whether residents can even afford to have a roof over their heads, and by that standard, California is failing.
A 2017 Harvard University report said that one-third of renters in the Los Angeles area are "severely rent burdened," meaning they spend at least half their income on housing. The median rent for a one-bedroom apartment in Los Angeles County has increased 67%, according to Zillow's Rent Index, the Los Angeles Times reports.
Homelessness has surged a stunning 75 percent in the last six years, the Los Angeles Times reports, and there are now at least 55,000 homeless people in the county.
U.S. News ranked every U.S. state in seven categories: health care, education, economy, opportunity, infrastructure, crime and corrections, and fiscal stability. California comes in 46th in "opportunity" and 43rd in "fiscal stability."
"North Dakota and Minnesota are the most effective at promoting their citizens' well-being by providing both a healthy environment and a sense of social connectedness. Other top states include Wisconsin, New Hampshire, South Dakota and Mississippi," the report said.
Iowa placed No. 1 in "quality of life."
The Daily Wire > Read > California Dead Last Among U.S. States In 'Quality Of Life,' Study Finds


text:
Q: Return each response from a loop I have an function using axios where I am deleting multiple records based on the number of ids returned for a specific user.
async function DeleteAllRecords (emailAddress) {
    try {
        var accessToken = await setup.getAccessToken(emailAddress);
        var userId = await user.getUserId(emailAddress);
        var recordIds = await getAllRecordID(emailAddress);
        console.log(`Deleting all records for `+emailAddress+``);
        for (const rId of recordIds) {
            const response = await axios.delete(`${process.env.API_URL}/`+userId+`/records/`+recordIds+``, {'headers': {Authorization: 'Bearer '+accessToken+''}});
        }
        return response;
    }
    catch(e) {
        console.error(``+emailAddress+` produced the Record Delete Error = ` + e);
    }
}

This isn't working, and I'm unsure why. I would like to see the response for each axios.delete call, but I'm not sure how to get that. Currently its returning as response undefined.

A: Why your code didn't work:

*

*const response is declared inside the loop scope, and is not accessible out of this closure.

*Even if it was defined before the loop (using let const), and assigned inside the loop, you would still be able to return only the last response.

You can push each response to an array (responses), and return the array:
async function DeleteAllRecords (emailAddress) {
    try {
        var accessToken = await setup.getAccessToken(emailAddress);
        var userId = await user.getUserId(emailAddress);
        var recordIds = await getAllRecordID(emailAddress);
        console.log(`Deleting all records for `+emailAddress+``);
        const responses = [];
        for (const rId of recordIds) {
            const response = await axios.delete(`${process.env.API_URL}/`+userId+`/records/`+recordIds+``, {'headers': {Authorization: 'Bearer '+accessToken+''}});
            responses.push(response);
        }
        return responses;
    }
    catch(e) {
        console.error(``+emailAddress+` produced the Record Delete Error = ` + e);
    }
}

However, in this case multiple parallel requests would be better, since you don't actually need to delete one by one. I would use Array.map() to iterate the recordIds array, and return a promise for each one, then wait for all responses using Promise.all(), which would also return an array of responses:

async function DeleteAllRecords (emailAddress) {
    try {
        var accessToken = await setup.getAccessToken(emailAddress);
        var userId = await user.getUserId(emailAddress);
        var recordIds = await getAllRecordID(emailAddress);
        console.log(`Deleting all records for `+emailAddress+``);

        return Promise.all(recordIds.map(rId =>  axios.delete(`${process.env.API_URL}/`+userId+`/records/`+recordIds+``, {'headers': {Authorization: 'Bearer '+accessToken+''}})));
    }
    catch(e) {
        console.error(``+emailAddress+` produced the Record Delete Error = ` + e);
    }
}

A:
This isn't working, and I'm unsure why. I would like to see the response for each axios.delete call, but I'm not sure how to get that. Currently its returning as response undefined.

There are several issues in your code:

*

*const response declared within loop block, but you try to return it after the loop. const and let are strictly block scoped, thus by referring to response after the loop block basically tells JS to return an undefined variable.

*You write several times to response. If the issue above wasnt in place, it would still not work correctly, since you only would end up with the response of the last loop run. Here you'd have to collect the response from all runs, e.g. into a list.

redpajama_set_name: RedPajamaStackExchange


text:
Home > Impact > Where We Work > Zambia
Bolivia En Español
Ecuador En Español
Guatemala En Español
Honduras En Español
Mexico En Español
Zambia, in southeastern Africa, is a large, sparsely populated country, with 46 percent of its population under the age of 15. Rural poverty and unemployment are significant problems. The nation faces several challenges, including more than 1.2 million people living with HIV and 380,000 children 17 and younger who were orphaned by AIDS. The Zambian economy grew gradually over the past decade, but in the past two years, low copper prices and poor harvests related to El Niño weather patterns have negatively impacted the economy.
SPONSOR NOW!
ChildFund has served children in Zambia since 1983. Help make a difference and sponsor a child in Zambia today.
Ages 0 – 5: Healthy and Secure
The mortality rate of children under 5 in Zambia is 87 children per 1,000 live births. ChildFund's primary concern is to make sure infants and toddlers receive care and good nutrition even before they're born. Community health workers, trained by ChildFund and our local partners, encourage mothers-to-be to attend prenatal clinics as soon as they learn they are pregnant, and educate them about the value of delivering at hospitals or health centers instead of at home. Once children are born, we provide growth monitoring to prevent malnutrition, vitamin supplements, deworming and vaccinations, and families receive treated mosquito nets to ward off malaria. In Luangwa, a region where we have offered health services for more than five years, infant mortality and malnutrition rates have decreased. We also work closely with Procter & Gamble's Children's Safe Drinking Water program to provide fresh water for families who don't live near a source of clean water. This benefits the youngest children in many ways.
Ages 6 – 14: Educated and Confident
ChildFund Zambia and our local partners work to improve school access and the quality of education by training children in the Child Friendly School concept, which encourages student participation. We have renovated classrooms to relieve congestion and provided water systems so children have clean restrooms and fresh drinking water. Schools have new desks, and students received better learning materials. As a result, absenteeism has fallen because students want to attend class and are more comfortable at school, and more than 80 percent of students in four Child Friendly Schools have passed to the next grade, up from 76 percent in 2013.
We work with community members (including children) to end violence that affects children where they live, where they attend school and many other places, and we've made child marriage a special focus because of its prevalence in Zambia. According to the United Nations, 42 percent of Zambian women ages 20 to 24 were married before the age of 18. By working with families and other community members, we hope to reduce the number of girls who are forced into early marriages that end their educations and put them at risk of abuse for the rest of their lives.
Ages 15 – 24: Skilled and Involved
Young people still have a difficult time entering Zambia's workforce unless they have specialized skills. ChildFund works to help youth gain experience in entrepreneurship, nursing, raising livestock, growing crops and fish farming, which are all viable fields of work in Zambia. At the same time as learning technical skills, youth enrolled in our programs also receive advice on saving money and spending it wisely. Most youth have opened bank accounts and are able to expand their businesses.
In collaboration with the Ministry of Health and with support from The MasterCard Foundation, ChildFund launched the Zambia Nurse and Life Skills Training Program, giving youth in rural areas access to nursing classes through e-learning. This program is helping solve Zambia's extreme shortage of healthcare workers while letting students continue to live at home instead of moving to a city for school. Last year, 66 students received scholarships. After five years, we expect that 6,000 young people will be trained as nurses and midwives.
Fighting Extreme Poverty in Zambia
Extreme poverty in Zambia causes numerous problems. According to 2015 statistics in the CIA World Factbook, more than a third of Zambians do not have access to improved water systems, a percentage that leaps to 48 percent in rural locations. The same is true for sanitation; 56 percent of Zambians — including 64 percent of rural residents — lack safe, clean toilets in or near their homes. These two obstacles alone cause disease, school absenteeism, shorter life spans and malnutrition. Zambia is considered a lower middle-income country, but this designation masks the poverty in rural areas, where unemployment is high, particularly for young people.
Despite these issues, Zambia has some net positives: a stable elected government and significant economic growth in its recent past. Not everyone sees the benefits because public debt is large, and its population suffers under the burden of an extremely high birth rate (an average of more than five children per woman) and a relatively high rate of HIV and AIDS.
ChildFund Zambia works with government ministries and other child-focused organizations to protect children's rights, including keeping them safe from abuse and early marriage. We also collaborate with other organizations to prevent the spread of AIDS, care for orphaned children, provide family-planning education and increase literacy and numeracy rates. Our youth-focused programs give teens and young adults the tools and training they need to find good jobs in Zambia's tight economy.
Treza
January 1 New Year's Day
March 12 Youth Day
May 1 Labor Day
May 25 African Freedom Day
July 1 Heroes Day
July 2 Unity Day
October 24 Independence Day
December 25 Christmas Day
Novel Bitterness
Novel A Cowrie of Hope
Short Fiction Eavesdropping
Documentary The Entrepreneurs
Documentary Where the Water Meets the Sky
Non-Fiction Boys to Men in the Shadow of AIDS
Music Zambia Roadside: Music From Southern Province
Cookbook Imperial African Cookery Book
Follow ChildFund's Zambia board on Pinterest.


text:
My E-mail: tryingtostaycalm@gmail.com
Click on my picture to view my profile
~Tooth Fairy 2 Movie Set Visit~
~My Flicka 3 Movie Set Visit~
I do not receive any money for my posts. I do however receive the review products at no charge to evaluate and express my opinion.
Echelon Conspiracy Blu-ray Review...
My Hubby and I got to review the Blu-ray Echelon Conspiracy. It starts off with Max Peterson getting a high tech cell phone. He starts getting text messages that he soon finds out come true. He starts winning big in a casino when the text tell him to bet big. The casino boss and the FBI start watching him and want to find out where the text messages are coming from. Max doesn't even know this. Dangerous security operatives chase the engineer across the globe, while a powerful government official pursues a mysterious agenda that will threaten the stability of the whole world. When they all find out where the messages are coming from, it brings you to the climax at the end of the movie. This was a pretty good movie.
It will be released on July 21st on DVD and Blu-ray by Paramount Home Entertainment. It features Shane West, Edward Burns, Ving Rhames, and Martin Sheen.
The ECHELON CONSPIRACY DVD is presented in widescreen enhanced for 16:9 televisions with Dolby Digital English 5.1 Surround and English, French and Spanish subtitles. The Blu-ray is presented in 1080p high definition with English 5.1 Dolby TrueHD and English, French, Spanish and English SDH subtitles.
ECHELON CONSPIRACY
My husband loves shows like this one!
Looks like an exciting movie
I want text messages like that!
Jolynn said...
This sounds like a action packed movie.
Wendyburd1 said...
This sounds so good!! And Hollywood Video won't have it, but Blockbuster will, thanks for letting me know about this movie!!
Enter my exciting current
Enter the $500 ZOOCCHINI giveaway here!
Trying To Stay Calm
This entire blog/website is @copyright protected by the owner and no portion may be used without permission. 2008-2019
Blog Archive July (1) September (2) August (9) July (2) January (2) December (1) November (3) October (6) September (3) July (2) June (9) May (2) April (1) March (1) February (3) January (6) December (5) November (4) September (2) August (8) July (1) June (2) May (4) April (2) March (1) December (4) November (12) October (6) September (6) August (2) July (1) May (4) April (11) March (4) February (2) January (2) December (9) November (9) October (8) September (6) August (12) July (14) June (16) May (15) April (16) March (10) December (3) November (4) October (14) September (2) August (1) July (1) June (1) May (1) April (1) March (3) February (4) January (4) December (11) November (13) October (4) September (7) August (6) July (12) June (5) May (6) April (6) March (10) February (6) January (4) December (4) November (15) October (17) September (19) August (19) July (19) June (16) May (16) April (28) March (11) February (15) January (9) December (14) November (24) October (23) September (23) August (21) July (16) June (17) May (17) April (17) March (21) February (19) January (24) December (18) November (22) October (32) September (37) August (28) July (35) June (18) May (17) April (35) March (26) February (20) January (20) December (26) November (19)
Click here to see more :)
Blogger Templates by Leelou Blogs


I'm a little late with today's "Thursday Talkback." It's been yet another crazy week at work and while the coming holiday on Monday is nice, it won't help with my workload.
With the price of gas steadily increasing, do you plan to modify your summer vacation plans??
Yep. We were planning a trip to Disney (haven't told the kids yet), but have adjusted to maybe just going halfway and hitting the beach in Ocean City, MD. Not a bad second choice though, and it will run us less than half of the original plans!
Not really. But only because we decided not to vacation until we had a rather large nest egg saved. We did not vacation last year either, but went to Maui the year before.
I have to work during the summer while people with kids leave the work for me. Fine with me because traveling in the off-season is cheaper and less-crowded.
I didn't really have any car travel plans. There may be a few plane trips for family events though.
We aren't traveling this summer, but my parents are driving here (1200 miles). My father's birthday and father's day will occur when they are here, so I plan on giving him a hefty gas gift card as a gift. Will help them get home.


"sitecopy is for easily maintaining remote web sites. The program will upload files to the server which have changed locally, and delete files from the server which have been removed locally, to keep the remote site synchronized with the local site with a single command."
There's a fink package for it, so apparently it's eminently portable to OS X, however, fink won't install it without several irrelevant "dependancies"... python, X11, and about 27 other packages that have nothing to do with this command-line C program.
I tried building it myself from source for OS X 10.1.5 and ran into a compiler error... that is, gcc reported an internal error with itself, so I'm stuck.