text:
\section{Introduction}

Integrating Description Logics (DLs) with rules for the Semantic Web has received considerable attention with approaches such as \emph{Description Logic Programs} \cite{grosof}, \emph{DL-safe rules} \cite{motik}, \ensuremath{\mathcal{DL}\text{+}\mathit{log}}{} \cite{rosati-kr2006}, \emph{dl-programs} \cite{eiter-ai2008}, \emph{Description Logic Rules} \cite{Krotzsch+Rudolph+Hitzler-DLRules:2008}, and Open Answer Set Programming (OASP) \cite{heymans-acm2008}. OASP is a formalism which combines attractive features from the Logic Programming (LP) and the DL world. The syntax and semantics of OASP build upon the syntax and semantics of Answer Set Programming (ASP) \cite{gelfond88stable}: there is a rule-based syntax with a \emph{negation as failure} operator which is interpreted via a stable model semantics, but unlike the LP setting,
an open domain semantics, like it is common in the DL world, is employed. This allows for stating generic knowledge, without the need to mention actual constants.

Several decidable fragments of OASP were identified by syntactically restricting the shape of logic programs, while carefully safe-guarding enough expressiveness for integrating rule- and ontology-based knowledge. A notable fragment is that of \emph{Forest Logic Programs (FoLPs)} \cite{heymans-jal2007} that are able to simulate reasoning in the DL $\mathcal{SHOQ}${}.
FoLPs allow for the presence of only unary and binary predicates in rules which have a tree-like structure. A sound and complete algorithm for satisfiability checking of unary predicates w.r.t. FoLPs has been presented in \cite{feier+heymans-HybridReasoningForestLogicPrograms:09}. The algorithm exploits the forest model property of the fragment: if a unary predicate is satisfiable, than it is satisfied by a forest-shaped model, with the predicate checked to be satisfiable being in the label of the root of one of the trees composing the forest. It is essentially a tableau-based procedure which builds such a forest model in a top-down fashion.

In this paper we describe an optimization for reasoning with FoLPs in the form of a knowledge compilation technique. The technique consists in pre-computing all possible building blocks of the tableau, in the form of trees of depth 1, blocks which we call \emph{unit completion structures}. The original algorithm is used for computing the unit completion structures. The revised algorithm matches and appends such building blocks until a termination condition is met, like blocking or reaching a certain depth in the tableau expansion.
In general, not all unit completion structures have to be considered: inherent redundancy in a FoLP, like rules which are less general than others gives rise to redundancy among completion structures. A unit completion structure is redundant iff there is another simpler (less constrained) unit completion structure. The latter can replace the former in any forest model. We formalize this notion, making it possible to identify such redundant structures and discard them.

The paper is structured as follows: Section \ref{sec:prelim} contains preliminaries, like the OASP semantics and some notation, and Section \ref{sec:FLP} introduces the FoLP fragment. An overview of the original algorithm for reasoning with FoLPs is given in Section \ref{sec:algorithm}. The main results of the paper concerning the computation of non-redundant unit completion structures, and the revised algorithm, are presented in Section \ref{sec:opt}. Finally, Section \ref{sec:discussion} draws some conclusions and discusses future work.

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

We recall the open answer set semantics \cite{heymans-acm2008}. \emph{Constants} $a,b,c,\ldots$, \emph{variables} $X,Y,\ldots$, \emph{terms} $s,t,\ldots$, and \emph{atoms} $p(t_1,\ldots,t_n)$ are as usual.
A \textit{literal} is an atom $L$ or a negated atom $\naf{L}$.  We allow for \emph{inequality literals} of the form $s\neq t$, where $s$ and $t$ are terms. A literal that is not an inequality literal will be called a \emph{regular literal}. For a set $S$ of literals or (possibly negated) predicates, $\posi{S} = \set{a \mid a \in S}$ and $\nega{S} = \set{a \mid \naf{a} \in S}$. For a set $S$ of atoms, $\naf{S} = \set{\naf{a} \mid a \in S}$.  For a set of (possibly negated) predicates $S$, $S(X) = \{a(X) \mid a \in S\}$ and $S(X,Y)=\{a(X,Y) \mid a \in S\}$. For a predicate $p$, $\pm p$ denotes $p$ or $\naf p $, whereby multiple occurrences of $\pm p$ in the same context will refer to the same symbol (either $p$ or $\naf p$).

A \textit{program} is a countable set of rules \prule{\alpha}{\beta}, where $\alpha$ is a finite set of regular literals and $\beta$ is a finite set
of literals. The set $\alpha$ is the \textit{head} and represents a disjunction, while $\beta$ is the \textit{body} and represents a conjunction.  If $\alpha =\emptyset$, the rule is called a \textit{constraint}. A special type of rules with empty bodies, are so-called \emph{free rules} which are rules of the form: ${q(t_1,\ldots,t_n)\lor\naf{q(t_1,\ldots,t_n)}\gets}{}$, for terms $t_1,\ldots,t_n$; these kind of rules enable a choice for the inclusion of atoms in the open answer sets. We call a predicate $q$ \emph{free} if there is a ${q(X_1,\ldots,X_n)\lor\naf{q(X_1,\ldots,X_n)}\gets}{}$, with variables $X_1,\ldots,X_n$. Atoms, literals, rules, and programs that do not contain  variables are \textit{ground}. For a rule or a program $R$, let $\cts{R}$ be the constants in $R$, $\vars{R}$ its variables, and $\preds{R}$ its predicates with $\upreds{R}$ the unary and $\bpreds{R}$ the binary predicates. For every non-free predicate $q$ and a program $P$, $P_q$ is the set of rules of $P$ that have $q$ as a head predicate.  A \emph{universe} $U$ for $P$ is a non-empty countable superset of the constants in $P$: $\cts{P} \subseteq U$. We call $\ground{P}{U}$ the ground program obtained from $P$ by applying all possible substitutions of variables by elements of $U$ to every rule in $P$. Let $\HB{P}$ ($\mathcal{L}_P$) be the set of regular atoms (literals) that can be formed from a ground program $P$.

An \textit{interpretation} $I$ of a ground $P$ is a subset of $\HB{P}$. We write $I\models p(t_1,\ldots,t_n)$ if $p(t_1,\ldots,t_n) \in I$ and $I \models \naf{p(t_1,\ldots,t_n)}$ if $I\not\models p(t_1,\ldots,t_n)$. Also, for ground terms $s,t$, we write
$I\models s\neq t$ if $s \neq t$. For a set of ground literals $L$, $I\models L$ if $I \models l$ for every $l \in L$.  A ground rule $r:\prule{\alpha}{\beta}$ is \textit{satisfied} w.r.t. $I$, denoted $I \models r$, if $I \models l$ for some $l \in \alpha$ whenever $I \models \beta$.  A ground constraint \prule{}{\beta} is satisfied w.r.t. $I$ if $I \not\models \beta$.

For a positive ground program $P$, i.e., a program without \ensuremath{\mathit{not}}, an interpretation $I$ of $P$ is a \textit{model} of $P$ if $I$ satisfies every rule in $P$; it is an \textit{answer set} of $P$ if it is a subset minimal model of $P$. For ground programs $P$ containing \ensuremath{\mathit{not}}, the \textit{GL-reduct} \cite{gelfond88stable} w.r.t. $I$ is defined as $P^I$, where $P^I$ contains \prule{\posi{\alpha}}{\posi{\beta}} for \prule{\alpha}{\beta} in $P$, $I \models \naf{\nega{\beta}}$ and $I \models \nega{\alpha}$.  $I$ is an \textit{answer set} of a ground $P$ if $I$ is an answer set of $P^I$.

A program is assumed to be a finite set of rules; infinite programs only appear as byproducts of grounding with an infinite universe. An \textit{open interpretation} of a program  $P$ is a pair $(U, M)$ where $U$ is a universe for $P$ and $M$ is an interpretation of $P_{U}$. An \textit{open answer set} of $P$ is an open interpretation $(U,M)$ of $P$ with $M$ an answer set of $\ground{P}{U}$. An $n$-ary predicate $p$ in $P$ is \emph{satisfiable} if there is an open answer set $(U,M)$ of $P$ s. t. $p(x_1,\ldots,x_n) \in M$, for some $x_1, \ldots, x_n \in U$.

We introduce notation for trees which extend those in \cite{Vardi98reasoningabout}. Let $\cdot$ be a concatenation operator between sequences of constants or natural numbers. A \emph{tree} $T$ with root $c$ ($T_c$), where $c$ is a specially designated constant, has as nodes sequences of the form $c \cdot s$, where $s$ is a (possibly empty) sequence of positive integers formed with the concatenation operator; for $x \cdot d\in T$, $d\in \N^{*}$, we have that $x\in T$. The set $A_{T}=\{(x,y) \mid x, y\in T, \Exists{n\in\N^{*}}{y=x \cdot n}\}$ is the set of arcs of a tree $T$. For $x,y\in T$, we say that $x <_T y$ iff $x$ is a prefix of $y$ and $x\neq y$.

A \emph{forest} $F$ is a set of trees $\{T_c \mid c \in C\}$, where $C$ is a set of distinguished constants. We denote with $N_F=\cup_{T\in F} T$ and $A_F=\cup_{T\in F}A_T$ the set of nodes and the set of arcs of a forest $F$, respectively. Let $<_F$ be a strict partial order relationship on the set of nodes $N_{F}$ of a forest $F$ where $x <_F y$ iff $x <_T y$ for some tree $T$ in $F$.  An extended forest $\ensuremath{\mathit{EF}}$ is a tuple $(F, \ensuremath{\mathit{ES}})$ where $F =\{T_c \mid c\in C\}$ is a forest and $\mathit{ES}\subseteq N_F\times C$. We denote by $N_{\ensuremath{\mathit{EF}}}=N_F$ the nodes of $\ensuremath{\mathit{EF}}$ and by $A_{\ensuremath{\mathit{EF}}}=A_F \cup \ensuremath{\mathit{ES}}$ its arcs. So unlike a normal forest, an extended forest can have arcs from any of its nodes to any root of some tree in the forest.

Finally, for a directed graph $G$, $paths_G$ is the set of pairs of nodes for which there exists a path in $G$ from the first node in the pair to the second one.

\section{Forest Logic Programs}\label{sec:FLP}

\emph{Forest Logic Programs (FoLPs)} \cite{heymans-jal2007} are logic programs with tree-shaped rules which allow for constants and for which satisfiability checking under the open answer set semantics is decidable.

\begin{definition}\label{def:FoLP} A \emph{forest logic program (FoLP)} is a program with only unary and binary predicates, and such that a rule is either
a \emph{free rule}
\prule{a(s)\lor \naf{a(s)}}{} or \prule{f(s,t)\lor \naf{f(s,t)}}{},
where $s$ and $t$ are terms such that if $s$ and $t$ are both variables, they are different,
a \textit{unary rule}
\begin{equation}\label{eq:unary}
r:\prule{a(s)}{\beta(s), (\gamma_m(s,t_m),\delta_m(t_m))_{1\leq m \leq k},\psi}
\end{equation}
where $s$ and $t_m$, $1\leq m \leq k$, are terms (again, if both $s$ and $t_m$ are variables, they are different; similarly for $t_i$ and $t_j$), where
\begin{itemize}
\item $\psi\subseteq \bigcup_{1\leq i\neq j\leq k}\set{t_i\neq t_j}$ and $\set{\neq} \cap \gamma_m = \emptyset$ for $1\leq m \leq k$,
\item $\Forall{t_i\in \vars{r}}{{\gamma_i^+}\neq\emptyset}$, i.e., for variables $t_i$ there is a positive atom that connects $s$ and $t_i$,
\end{itemize} or a \emph{binary rule}
\begin{equation}\label{eq:binary}
\prule{f(s,t)}{\beta(s), \gamma(s,t), \delta(t)}
\end{equation}
with $\set{\neq}\cap \gamma = \emptyset$ and $\posi{\gamma} \neq \emptyset$ if $t$ is a variable ($s$ and $t$ are different if both are variables),
or a \textit{constraint}
\prule{}{a(s)} or\prule{}{f(s,t)}
where $s$ and $t$ are different if both are variables).
\end{definition}

The following program $P$ is a FoLP which says that an individual is a special member of an organization (\emph{smember}) if it has the support of another special member: \emph{rule} $r_1$, or if it has the support of two regular members of the organization (\emph{rmember}): \emph{rule} $r_2$. The binary predicate \emph{support} which describes the `has support' relationship is free. Nobody can be at the same time both a special member or a regular member: \emph{constraint} $r_4$. Two particular regular members are $a$ and $b$: \emph{facts} $r_5$ and $r_6$.

\begin{example}\label{ex:FoLP}
\small
\begin{programn}
\label{folp}
\nrule{r_1}{smember(X)}{support(X,Y), smember(Y)}
\nrule{r_2}{smember(X)}{support(X,Y), rmember(Y),}
&&&\ensuremath{support(X,Z), rmember(Z), Y \neq Z}\\
\nrule{r_3}{support(X, Y) \lor \naf{support(X,Y)}} {}
\nrule{r_4} {} {smember(X), rmember(X)}
\nrule{r_5}{rmember(a)}{}
\nrule{r_6}{rmember(b)}{}
\end{programn}
\normalsize
\end{example}

As their name suggests FoLPs have the \emph{forest model property}:

\begin{definition}\label{def:forest-sat1}
Let $P$ be a program.
A predicate $p\in \upreds{P}$ is \emph{forest satisfiable}\index{forest satisfiable} w.r.t. $P$ if there is an open answer set $(U,M)$ of $P$ and there is an extended forest
$\ensuremath{\mathit{EF}} \equiv (\set{T_{\varepsilon}} \cup \set{T_a \mid a \in \cts{P}},\ensuremath{\mathit{ES}})$, where $\varepsilon$ is a constant, possibly one of the constants appearing in $P$
, and a labeling function
$\mathcal{L}:\set{T_{\varepsilon}} \cup \set{T_a \mid a \in \cts{P}}\cup A_{\ensuremath{\mathit{EF}}} \to 2^{\preds{P}}$ s. t.
\begin{itemize}
\item $U = N_{\ensuremath{\mathit{EF}}}$, and
\item $p \in \mathcal{L}(\varepsilon)$,
\item $z \cdot i \in T\in \ensuremath{\mathit{EF}}$, $i > 0$, iff there is some $f(z,z\cdot i) \in M$, $z\in T$, and
\item for $y \in T\in \ensuremath{\mathit{EF}}$, $q \in \upreds{P}$, $f \in \bpreds{P}$,
we have that
	\begin{itemize}
	\item $q(y) \in M$ iff $q \in \mathcal{L}(y)$, and
	\item $f(y,u) \in M$ iff $(u = y\cdot i \lor u \in \cts{P}) \land f \in \mathcal{L}(y,u)$.
	\end{itemize}
\end{itemize}

We call such a $(U,M)$ a \emph{forest model} and a program $P$ has the \emph{forest model property} if the following property holds: if $p \in \upreds{P}$ is satisfiable w.r.t. $P$ then $p$ is forest satisfiable w.r.t. $P$.
\end{definition}

Consider the FoLP $P$ introduced in Example \ref{ex:FoLP}. The unary predicate $smember$ is forest satisfiable w.r.t. $P$: $(\{a,b,x\},$ $ \{rmember(a),$ $ rmember(b), $ $support (x,a),$ $support(x,b),$ $smember(x)\})$ is a forest model in which $smember$ appears in the label of the (anonymous) root of one of the trees in the forest (see Figure 1). Note that in the ordinary LP setting, where one restricts the universe to the Herbrand universe, $smember$ is not satisfiable.

\vspace{-8mm}
\small
\begin{center}
\label{fig:forestmodel}
\begin{figure}
\begin{tikzpicture}[level distance=3.5cm, >=stealth']

    \node(x){$x$}
          child[grow=left]{
                node (a) {$a$}
		        edge from parent [->]
       	         	node[below,near end, xshift=0.5cm] {$\{support\}$}
          }
	  child[grow=right]{
		node (b) {$b$}
		        edge from parent [->]
       	         	node[below,near end, xshift=-0.5cm] {$\{support\}$}
          };

    \node[right, xshift=-1.2cm, yshift=0.35cm] at (x.east) {$\{smember\}$};
    \node[right, xshift=-2.1cm] at (a.east) {$\{rmember\}$};
    \node[right, xshift=-0.2cm] at (b.east) {$\{rmember\}$};
    \end{tikzpicture}
    \vspace{-2mm}
    \caption{A Forest Model for $P$}
\end{figure}
\end{center}
\normalsize
\vspace{-18mm}

\section{An Algorithm for Forest Logic Programs}\label{sec:algorithm}

In this section, we give an overview of the tableau algorithm for satisfiability checking for FoLPs introduced in \cite{feier+heymans-HybridReasoningForestLogicPrograms:09}. For technical details we refer the reader to the original paper. We use as a running example the FOLP from Example \ref{ex:FoLP}. Constraints are not treated explicitly in the algorithm as they can be simulated using unary rules. As such, the constraint $\nprule{r_4}{}{smember(X), rmember(X)}$ in Example \ref{ex:FoLP} is replaced with $\nprule{r'{_4}}{co(X)} {\naf{co}(X), smember(X), rmember(X)}$, with $\mathit{co}$ a new predicate.

The basic data structure used by the algorithm is a so-called  \emph{completion structure}. It contains an extended forest $EF$, whose set of nodes constitutes the universe of the model, and a labeling function $\ensuremath{\mathsc{ct}}$ (\textit{content}), which assigns to every node, resp. arc of $EF$, a set of possibly negated unary, resp. binary predicates. The presence of a predicate symbol $p/\naf p$ in the content of some node or arc $x$ indicates the presence/absence of the atom $p(x)$ in the open answer set. The presence (absence) of an atom in the open answer set is justified by imposing that the body of at least one ground rule which has the respective atom in the head is satisfied (no body of a rule which has the respective atom in the head is satisfied). In order to keep track which (possibly negated) predicate symbols in the content of some node or arc have already been expanded a completion structure contains also a so-called status function \ensuremath{\mathsc{st}}. Furthermore, in order to ensure that no atom in the partially constructed open answer set is circularly motivated, i.e. the atoms are well-supported \cite{fages-NewfixpointSem:91}, a graph $G$ which keeps track of dependencies between atoms in the (partial) model is maintained.

\begin{definition}\label{def:completionstructure} An $\mathcal{A}_1$-\textit{completion structure for a FoLP $P$}\footnote{We use the prefix $\mathcal{A}_1$ to denote completion structures computed using this original algorithm as opposed to completion structures computed using the optimised algorithm described in the next section for which we will use the prefix $\mathcal{A}_2$.} is a tuple $\langle \ensuremath{\mathit{EF}},$ $\ensuremath{\mathsc{ct}},$ $\ensuremath{\mathsc{st}},$ $G \rangle$
where:
\begin{itemize}
\item $\ensuremath{\mathit{EF}}=\langle F,\ensuremath{\mathit{ES}} \rangle$ is an extended forest,
\item $\ensuremath{\mathsc{ct}}:N_{\ensuremath{\mathit{EF}}} \cup A_{\ensuremath{\mathit{EF}}} \to 2^{preds (P) \cup \naf{(preds(P))}}$ is the `content' function,
\item $\ensuremath{\mathsc{st}}:\{(x, \pm q) \mid \pm q \in \ensuremath{\mathsc{ct}}(x), x \in N_{\ensuremath{\mathit{EF}}} \cup A_{\ensuremath{\mathit{EF}}}\} \to \{\ensuremath{\mathit{exp}}, \ensuremath{\mathit{unexp}}\}$
is the `status' function,
\item $G=\grap{V}{A}$ is a directed graph which has as vertices atoms in the answer set in construction: $V \subseteq \HB{\ground{P}{N_{\ensuremath{\mathit{EF}}}}}$.
\end{itemize}

An \emph{initial $\mathcal{A}_1$-completion structure} for checking satisfiability of a unary predicate $p$ w.r.t. a FoLP $P$ is a completion structure $\langle \ensuremath{\mathit{EF}},$ $\ensuremath{\mathsc{ct}},$ $\ensuremath{\mathsc{st}},$ $G \rangle$ with $\ensuremath{\mathit{EF}}=(F,\emptyset)$, $F=\set{T_{\varepsilon}} \cup \set{T_a \mid a \in \cts{P}}$, where $\varepsilon$ is a constant, possibly in $\cts{P}$, $T_x=\{x\}$, for $x \in \{\varepsilon\} \cup \cts{P}$, $G=\grap{V}{\emptyset}$, $V=\{p(\varepsilon)\}$, and $\ensuremath{\mathsc{ct}}(\varepsilon)=\{p\}$, $\ensuremath{\mathsc{st}}(\varepsilon,p)=\ensuremath{\mathit{unexp}}$.
\end{definition}

An extended forest is initialized with single-node trees having as roots constants from $P$ and, possibly, a new single-node tree with anonymous root.
The forest model from Figure 1 has been evolved from an initial completion structure which has as $\varepsilon$, the root element where $smember$ has to be satisfied, the anonymous individual, $x$. There are two other single-node trees: $T_a$ and $T_b$. The predicate $smember$ in the content of $x$ is marked as unexpanded and $G$ is a graph with a single vertex $smember(x)$.

\vspace{1mm}
\small
\begin{center}
\begin{tabular}{ll}
$EF$:&
\begin{tikzpicture}[level distance=3.5cm, >=stealth']

    \node[yshift=-0.35cm](x){$x$};
    \node[xshift=-3.5cm](a) at (x.west) {$a$};
    \node[xshift=3.5cm](b) at (x.east) {$b$};
    \node[right, xshift=-1.2cm, yshift=0.35cm] at (x.east) {$\{smember^u\}$};
    \node[right, xshift=-0.2cm] at (a.east) {$\{\}$};
    \node[right, xshift=-0.2cm] at (b.east) {$\{\}$};
    \end{tikzpicture}
     \vspace{2mm} \\ $V$: & $smember(x)$ \\
$A$: & $\emptyset$
\end{tabular}
\end{center}
\normalsize

An initial $\mathcal{A}_1$-completion structure for checking the satisfiability of a unary predicate $p$ w.r.t. a FoLP $P$ is evolved by means of \emph{expansion rules} to a complete clash-free structure that corresponds to a finite representation of an open answer set in case $p$ is satisfiable w.r.t. $P$. \emph{Applicability rules} govern the application of the expansion rules.

\subsection{Expansion Rules}\label{sec:expansionrules}

In the following, for a completion structure $\langle \ensuremath{\mathit{EF}},$ $\ensuremath{\mathsc{st}},$ $\ensuremath{\mathsc{ct}},$  $G \rangle$, let $x \in N_{\ensuremath{\mathit{EF}}}$ and $(x,y)\in A_{\ensuremath{\mathit{EF}}}$ be the node, resp. arc, under consideration.

\textbf{\emph{(i) Expand unary positive}}. For a unary positive (non-free) $p \in \ensuremath{\mathsc{ct}}(x)$ s. t. $\ensuremath{\mathsc{st}}(x,p)=\ensuremath{\mathit{unexp}}$,
choose a unary rule $r\in P_p$
 for which $s$, the head term, matches $x$; ground this rule by substituting $s$ with $x$, in case $s$ is a variable, and every successor term  $t_m$ which is a variable with a successor of $x$ in $EF$ s. t. the inequalities in $\psi$ are satisfied (if needed one can introduce new successors of $x$ in $EF$, either as successors of $x$ in $T$, where $x \in T$, or in the form of constants from $P$). We motivate the presence of $p(x)$ in the open answer set by enforcing its body to be satisfied by inserting appropriate (possibly negated) predicate symbols in the contents of nodes/arcs of the structure. The newly inserted predicate symbols are marked as unexpanded and $G$ is updated, by adding arcs from $p(x)$ to every body atom.

In our example, $smember$ is unexpanded in the initial completion structure. Rule $r_2$ is chosen to motivate the presence of $smember(x)$ in the open answer set. It is grounded by substituting $X$ with $x$, and $Y_1$ and $Y_2$ with $a$ and $b$, respectively:  $\prule{smember(x)}{support(x,a)}$ $, rmember(x,a),$ $support(x,b), rmember(x,b)$. We enforce the body of this ground rule to be true and obtain the following completion structure (note also that $G$ has been updated):

\small
\begin{center}
\begin{tabular}{ll}
$EF$:\hspace{1mm}& \hspace{1mm}
\begin{tikzpicture}[level distance=3.5cm, >=stealth']

    \node(x)[yshift=-0.35cm]{$x$}
          child[grow=left]{
                node (a) {$a$}
		        edge from parent [->]
       	         	node[below,near end, xshift=0.5cm] {$\{support^{u}\}$}
          }
	  child[grow=right]{
		node (b) {$b$}
		        edge from parent [->]
       	         	node[below,near end, xshift=-0.5cm] {$\{support^{u}\}$}
          };

    \node[right, xshift=-1.2cm, yshift=0.35cm] at (x.east) {$\{smember^{e}\}$};
    \node[right, xshift=-2.2cm] at (a.east) {$\{rmember^{u}\}$};
    \node[right, xshift=-0.2cm] at (b.east) {$\{rmember^{u}\}$};
    \end{tikzpicture}
     \vspace{2mm}
 \\
    $V:$\hspace{1mm} &\hspace{1mm}$smember(x), support(x,a), support(x, b), rmember(x, a), rmember(x,b)$
\\
    $A:$\hspace{1mm} &\hspace{1mm}$smember(x) \rightarrow support(x,a), smember(x) \rightarrow support(x,b),$\\
    &\hspace{1mm}$smember(x) \rightarrow rmember(x,a),$ $smember(x) \rightarrow rmember(x,b)$
\end{tabular}
    \end{center}
\vspace{-1mm}
\normalsize

 All currently unexpanded predicates, i.e., $support$ in the content of arcs $(x,a)$ and $(x,b)$, and $rmember$ in the content of nodes $a$ and $b$,  can be trivially expanded as $support$ is a free predicate and $r_5$ and $r_6$ are facts. However one still has to ensure that the structure constructed so far can be extended to an actual open answer set, i.e., it is consistent with the rest of the program. The following expansion rule takes care of this.

\textbf{\emph{(ii) Choose a unary predicate}}. If all predicates in $\ensuremath{\mathsc{ct}}(x)$ and in the contents of x's outgoing edges are expanded and there are still unary predicates $p$ which do not appear in $\ensuremath{\mathsc{ct}}(x)$, pick such a $p$ and inject either $p$ or $\naf p$ in $\ensuremath{\mathsc{ct}}(x)$. The intuition is that one has to explore all unary/binary predicates at every node/arc as some predicate which is not reachable by dependency-directed expansion can prohibit the extension of the partially constructed model to a full model. Consider the simple case where there is a predicate $p$ defined only by the rule: $\prule{p}{\naf p}$ and $\pm p$ does not appear in the body of any other rule. The program is obviously inconsistent, but this cannot be detected without trying to prove that $p$ is or is not in the open answer set.

In our example, one does not know whether $co$ or $\naf{co}$ belongs to $\ensuremath{\mathsc{ct}}(x)$. We choose to inject $\naf{co}$ in $\ensuremath{\mathsc{ct}}(x)$ and mark it as unexpanded.

\textbf{\emph{(iii) Expand unary negative}}. Justifying a negative unary predicate $\naf p \in \ensuremath{\mathsc{ct}}(x)$ means refuting the body of every ground rule which defines $p(x)$, or in other words refuting at least a literal from the body of every ground rule which defines $p(x)$.
For more technical details concerning this rule we refer the reader to \cite{feier+heymans-HybridReasoningForestLogicPrograms:09}.

In our example, the unexpanded predicate in $\ensuremath{\mathsc{ct}}(x)$, $\naf{co}$, is defined by one rule, $r'{_4}$, whose only possible grounding is $\prule{co(x)} {\naf{co}(x), smember(x), rmember(x)}$. Refuting the body of this rule amounts to inserting $\naf{rmember}$ in $\ensuremath{\mathsc{ct}}(x)$ ($smember$ and $\naf{co}$ are already part of the content of that node). At its turn, the presence of $\naf{rmember}$ in $\ensuremath{\mathsc{ct}}(x)$ has to be motivated by using the expand unary negative rule, and the process goes on. Finally, we obtain a completion structure in which no expansion rule is further applicable and which represents exactly the forest model from Figure 1 ($smember$ and $rmember$ are abbreviated with $sm$ and $rm$, respectively):

\vspace{-3mm}
\small
\begin{center}
\begin{tabular}{ll}
$EF$:& \begin{tikzpicture}[level distance=4.2cm, >=stealth']

    \node(x)[yshift=-0.35cm, xshift=-2.0cm]{$x$}
          child[grow=left]{
                node (a) {$a$}
		        edge from parent [->]
       	         	node[below,near end, xshift=1.7cm] {$\{support\}$}
          }
	  child[grow=right]{
		node (b) {$b$}
		        edge from parent [->]
       	         	node[below,near end, xshift=-1.7cm] {$\{support\}$}
          };

    \node[right, xshift=-1.7cm, yshift=0.35cm] at (x.east) {$\{sm, \naf{rm}, \naf{co}\}$};
    \node[right, xshift=-1.7cm, yshift=-0.35cm] at (a.east) {$\{rm, \naf{sm}, \naf{co}\}$};
    \node[right, xshift=-1.7cm, yshift=-0.35cm] at (b.east) {$\{rm, \naf{sm}, \naf{co}\}$};
    \end{tikzpicture}
     \vspace{2mm}
 \\
    $V:$&$sm(x), support(x,a), support(x, b), rm(x, a),$ $rm(x,b)$

\\
    $A:$&$sm(x) \rightarrow support(x,a), sm(x) \rightarrow support(x,b),$
    $sm(x) \rightarrow rm(x,a),$ $sm(x)$ $\rightarrow rm(x,b)$
\end{tabular}
    \end{center}
\vspace{0mm}
\normalsize

Similarly to rules (i), (ii), and (iii) we define the expansion rules for binary predicates: (iv) \emph{Expand binary positive}, (v) \emph{Expand binary negative}, and (vi) \emph{Choose binary}.

\subsection{Applicability Rules}\label{sec:appl}

The applicability rules restrict the use of the expansion rules.

\textbf{\emph{(vii) Saturation}.} A node $x \in N_{\ensuremath{\mathit{EF}}}$ is \emph{saturated} if for all ${p \in \upreds{P}}$, $p \in \ensuremath{\mathsc{ct}}(x)$ or $\naf p \in \ensuremath{\mathsc{ct}}(x)$, and no $\pm q \in \ensuremath{\mathsc{ct}}(x)$ can be expanded with rules (i-iii), and for all ${(x,y) \in A_{\ensuremath{\mathit{EF}}}}$ and $p \in \bpreds{P}$, $p \in \ensuremath{\mathsc{ct}}(x,y)$ or $\naf p \in \ensuremath{\mathsc{ct}}(x,y)$, and no $\pm f \in \ensuremath{\mathsc{ct}}(x,y)$ can be expanded with (iv-vi). No expansions should be performed on a node from $N_{\ensuremath{\mathit{EF}}}$ which does not belong to $\cts{P}$ until its predecessor is saturated.

\textbf{\emph{(viii) Blocking}.} A node $x \in N_\ensuremath{\mathit{EF}}$ is \emph{blocked} if there is an ancestor $y$ of $x$ in $F$, $y<_F x$, $y \not \in \cts{P}$, s. t. $\ensuremath{\mathsc{ct}}(x) \subseteq \ensuremath{\mathsc{ct}}(y)$ and the set $paths_G(y,x)=\{(p,q) \mid (p(y), q(x)) \in paths_G \wedge q \mbox{ is not free}\}$ is empty. We call $(y,x)$ a \emph{blocking pair}. No expansions can be performed on a blocked node. One can notice that subset blocking is not enough for pruning the tableau expansion. Every atom in the open answer set has to be finitely motivated \cite[Theorem 2]{heymans-amai2006}: in order to ensure that, one has to check that there is no dependency in $G$ between an atom formed with the blocking node and an atom formed with the blocked node. The extra condition makes the blocking rule insufficient to ensure the termination of the algorithm. The following applicability rule ensures termination.

\begin{example}\label{ex:blocking}
Consider a restricted version of $P$ from Example \ref{ex:FoLP} which contains only rules $r_1$, and $r_3$. By checking satisfiability of $smember$ w.r.t. the new program one obtains the following completion structure:\newline
\small
\begin{center}
\begin{tabular}{lll}
$EF$: \hspace{10mm}
&
$V:\{smember(x), smember(y)\}$&\hspace{2mm}
$A:\{smember(x) \to smember(y)\}$
\\
\begin{tikzpicture}[ auto]

    \node (x) {$x$}
          child{
                node (y) {$y$}
		edge from parent [->]
		};
    	\node[yshift=-0.6cm, xshift=0.8cm] {$\{support\}$};
     \node[right, xshift=-0.2cm] at (x.east) {$\{smember\}$};
    \node[right, xshift=-0.2cm] at (y.east) {$\{smember\}$};
\end{tikzpicture}
&&
\end{tabular}
\end{center}
\normalsize
While the contents of nodes $x$ and $y$ are identical, they do not form a blocking pair as there is an arc in $G$ between $smember(x)$ and $smember(y)$: unfolding the structure (justifying $y$ similarly as $x$) would lead to an infinite chain: $smember(x), $ $smember(y), $ $smember(z), \ldots,$ in the atom dependency graph of the grounded program.
\end{example}

\textbf{\emph{(ix) Redundancy}.} A node $x \in N_\ensuremath{\mathit{EF}}$ is \emph{redundant} if it is saturated, it is not blocked, and there are $k$ ancestors of $x$ in $F$, $(y_i)_{1 \leq i \leq k}$, with $k=2^p(2^{p^2}-1)+3$, and $p=|\upreds{P}|$, s. t. $\ensuremath{\mathsc{ct}}(x)=\ensuremath{\mathsc{ct}}(y_i)$. In other words, a node is redundant if it is not blocked and it has $k$ ancestors with content equal to its content: any forest model of a FoLP $P$ which satisfies $p$ can be reduced to another forest model which satisfies $p$ and has at most $k+1$ nodes with equal content on any branch of a tree from the forest model, and furthermore the $(k+1)st$ node, in case it exists, is blocked \cite{feier+heymans-HybridReasoningForestLogicPrograms:09}. One can thus search for forest models only of the latter type. As such the detection of a redundant node constitutes a clash and stops the expansion process.

\subsection{Termination, Soundness, Completeness, Complexity Results}

An $\mathcal{A}_1$-completion structure is \emph{contradictory} if for some $x \in N_ {\ensuremath{\mathit{EF}}}/A_{\ensuremath{\mathit{EF}}}$ and $p \in \upreds{P}/$ $\bpreds{P}$, $\{p, \naf p\} \subseteq \ensuremath{\mathsc{ct}}(x)$. An $\mathcal{A}_1$-completion structure for a FoLP $P$ and a $p\in\upreds{P}$ is \emph{complete} if it is a result of applying the expansion rules to the initial completion structure for $p$ and $P$, taking into account the applicability rules, s. t. no expansion rules can be further applied.

Also, a complete $\mathcal{A}_1$-completion structure  $\ensuremath{\mathit{CS}} = \langle \ensuremath{\mathit{EF}},$ $\ensuremath{\mathsc{ct}},$ $\ensuremath{\mathsc{st}},$ $G \rangle$ is $\mathcal{A}_1$-\emph{clash-free} if:
 (1) \ensuremath{\mathit{CS}}{} is not contradictory
 (2) $\ensuremath{\mathit{EF}}$ does not contain redundant nodes
 (3) $G$ does not contain cycles (4) there is no $p \in \upreds{P}/\bpreds{P}$ and $x \in N_ {\ensuremath{\mathit{EF}}}/A_{\ensuremath{\mathit{EF}}}$, $x$ unblocked, s.t. $p \in \ensuremath{\mathsc{ct}}(x)$, and $\ensuremath{\mathsc{st}}(x,p)=\ensuremath{\mathit{unexp}}$.

It has been shown that an initial $\mathcal{A}_1$-completion structure for a unary predicate $p$ and a FoLP $P$ can always be expanded to a complete $\mathcal{A}_1$-completion structure (\emph{termination}), that, if $p$ is satisfiable w.r.t. $P$, there is a complete clash-free $\mathcal{A}_1$-completion structure (\emph{soundness}), and, finally, that, if there is a complete clash-free $\mathcal{A}_1$-completion structure, $p$ is satisfiable w.r.t. $P$ (\emph{completeness}).

In the worst case the algorithm runs in double exponential time, and a complete completion structure has a double exponential number of nodes in the size of the program. The high complexity is mostly due to the fact that blocking is not enough to ensure termination, and that, in particular, ``anywhere blocking''\cite{Motik+Shearer+Horrocks:DLReasHypertableaux} cannot be used as a termination technique. As already explained this peculiarity appears as a result of adopting a minimal model semantics.

\section{Optimized Reasoning with FoLPs}
\label{sec:opt}

This section presents a knowledge compilation technique for reasoning with FoLPs together with an algorithm which makes use of this pre-compiled knowledge. The main idea is to capture all possible local computations, which are typically performed over and over again in the process of saturating the content of a node, by pre-computing all possible completion structures of depth 1 using the original algorithm described in the previous section.
In the new algorithm, saturating the content of a node reduces to picking up one of the pre-computed structures which satisfies the existing constraints regarding the content of that node and appending the structure to the completion in construction: such constraints are sets of unexpanded (possibly negated) predicates which are needed to motivate the presence/absence in the open answer set of atoms constructed with the current node and the node above it.

Picking up a certain unit completion structure to saturate a node can impose strictly more constraints on the resulted structure than picking another unit completion structure with the same root content. Such constraints refer to: (1) the contents of the successor (non-blocked) nodes in a unit completion structure; (2)  the paths from an atom formed with the root node of a unit completion to an atom formed with a successor node of such a completion -- the more paths there are the harder blocking becomes. We discard such structures which are strictly more constraining than others, as they can be seen as redundant building blocks for a model.

The rest of the section formalizes and exemplifies these notions.

\subsection{Unit Completion Structures}

As mentioned in the introduction of this section, the intention is to obtain all completion structures of depth 1 which can be used as building blocks in our algorithm. We call such structures \emph{unit completion structures}. The skeleton of such a structure, is a so-called \emph{initial unit completion structure}. If they are to be used as building blocks in the algorithms, unit completion structures have to have as backbones trees of depth 1, and not forests. Hence, an initial unit completion structure is defined as a tree (unlike its counterpart notion from the previous section, initial completion structure, which is defined as a forest) with a single node, the root, which is either an anonymous constant or one of the constants already present in the program. The content of the root is empty.

\begin{definition}\label{def:initunitcomplstr}
An \emph{initial unit completion structure} for a FoLP $P$ is a completion structure $\langle \ensuremath{\mathit{EF}},$ $\ensuremath{\mathsc{ct}},$ $\ensuremath{\mathsc{st}},$ $G\rangle$ with $\ensuremath{\mathit{EF}}=(F,\ensuremath{\mathit{ES}})$, $F=\set{T_{\varepsilon}}$, where $\varepsilon$ is a constant, possibly in $\cts{P}$, $T_{\varepsilon}=\{\varepsilon\}$, $\ensuremath{\mathit{ES}}=\emptyset$, $G=\grap{V}{A}$, $V=\emptyset$, $A=\emptyset$, and $\ensuremath{\mathsc{ct}}(\varepsilon)=\emptyset$.
\end{definition}

A unit completion structure captures a possible local computation: that is, it is obtained as an expansion of an initial unit completion structure, to a tree of depth 1.

\begin{definition}\label{def:unitcomplstr}
A \emph{unit completion structure} $\langle \ensuremath{\mathit{EF}},$ $\ensuremath{\mathsc{ct}},$ $\ensuremath{\mathsc{st}},$ $G \rangle$ for a FoLP $P$, with $\ensuremath{\mathit{EF}}=(\set{T_{\varepsilon}},\ensuremath{\mathit{ES}})$,  is an $\mathcal{A}_1$-completion structure derived from an initial unit completion structure by application of the expansion rules (i)-(vi) described in Section \ref{sec:expansionrules}, according to the applicability rules introduced in Section \ref{sec:appl}, which has been expanded such that $\varepsilon$ is saturated and for all $s$ such that $\varepsilon \cdot s \in T_{\varepsilon}$, and for all $\pm p \in \ensuremath{\mathsc{ct}}(\varepsilon \cdot s)$, $\ensuremath{\mathsc{st}}(\pm p, \varepsilon \cdot s)=\ensuremath{\mathit{unexp}}$.\footnote{The status function is relevant only in the definition/construction of a unit completion structure, but not in the context of using such structures. As such, we will denote a unit completion structure in the following as a triple $\langle \ensuremath{\mathit{EF}},$ $\ensuremath{\mathsc{ct}},$ $G \rangle$.}
\end{definition}

\begin{example}\label{ex:threeucps}

Consider the program $Pr$:

\begin{programn}
\label{folp2}
\nrule{r_1}{p(X)}{\naf{p(X)}}
\nrule{r_2}{p(X)}{f(X,Y), \naf{q(Y)}}
\nrule{r_3}{p(X)}{f(X,Y), p(Y)}
\nrule{r_4}{p(X)}{f(X,Y), \naf{q(Y)}, p(Y)}
\nrule{r_5}{q(X)}{f(X,Y), \naf{p(Y)}}
\nrule{r_6}{f(X,Y) \lor \naf{f(X,Y)}}{}
\end{programn}

\end{example}
Figure 2 depicts three unit completion structures for $Pr$. They all have the same content for the root node: $\{p, \naf{q}\}$. The presence of $p$ in the content of the root node has been motivated in the first structure by means of rule $r_4$, in the second structure by means of rule $r_3$, and in the third structure by means of rule $r_2$. The different ways to derive $p$ lead to different sets of arcs in the dependency graphs belonging to each structure. On the other hand, to motivate that $\naf{q}$ is in the content of the root node, in each case it was shown that the body of $r_5$ grounded such that $X$ is instantiated as the root node and $Y$ as the successor node is not satisfied, or more concretely the presence of $p$ in the content of the successor node was enforced in each case ($\naf{f}$ could not be used to invalidate the triggering of the rule as $f$ was already present in the content of the arc from the root node to the successor node in each case).

\begin{figure}
\vspace{3mm}
\small
\begin{center}
\begin{tabular}{l|l|l}
\hspace{1mm}
$UC_1:$&
\hspace{1mm}
$UC_2:$&
\hspace{1mm}
$UC_3:$
\\
\hspace{1mm}
\begin{tikzpicture}[ auto]
    \node (x) {$a$}
          child{
            node (y) {$a1$}
		    edge from parent [->]
            node[above,near end,xshift=0.3cm] {$\{f\}$}
            };
    \node[right, xshift=-0.2cm] at (x.east) {$\{p, \naf{q}\}$};
    \node[right, xshift=-0.2cm] at (y.east) {$\{p, \naf{q}\}$};
    \end{tikzpicture}
&
\hspace{1mm}
 \begin{tikzpicture}[ auto]
    \node (x) {$b$}
          child{
            node (y) {$b1$}
		    edge from parent [->]
            node[above,near end,xshift=0.3cm] {$\{f\}$}
            };
    \node[right, xshift=-0.2cm] at (x.east) {$\{p, \naf{q}\}$};
    \node[right, xshift=-0.2cm] at (y.east) {$\{p \}$};
    \end{tikzpicture}
&
\hspace{1mm}
\begin{tikzpicture}[ auto]
    \node (x) {$c$}
          child{
            node (y) {$c1$}
		    edge from parent [->]
            node[above,near end,xshift=0.3cm] {$\{f\}$}
            };
    \node[right, xshift=-0.2cm] at (x.east) {$\{p, \naf{q}\}$};
    \node[right, xshift=-0.2cm] at (y.east) {$\{p, \naf{q}\}$};
\end{tikzpicture}
\\
\hline
\hspace{2mm}
$G_1=(V_1, A_1)$&
\hspace{2mm}
$G_2=(V_2, A_2)$&
\hspace{2mm}
$G_3=(V_3, A_3)$
\\
& & \\

\hspace{2mm}
$V_1:p(a), p(a1), f(a, a1)$&
\hspace{2mm}
$V_2:p(b), p(b1), f(d, d1)$&
\hspace{2mm}
$V_3:p(c), p(c1), f(c, c1)$\\
&&\\
\hspace{2mm}
\multirow{2}{*}{$A_1:$}
$p(a) \rightarrow f(a,a1),$&
\hspace{2mm}
\multirow{2}{*}{$A_2:$}
$p(b)\rightarrow f(b,b1),$&
\hspace{2mm}
\multirow{2}{*}{$A_3:p(c)\rightarrow f(c,c1)$}\\
\hspace{8.5mm} $p(a) \rightarrow p(a1)$ &
\hspace{8.5mm} $p(b)\rightarrow p(b1)$\\
\end{tabular}
\vspace{2mm}
\label{figure:threeucps}
\caption{Three unit completion structures for $Pr$: $UC_1$, $UC_2$, and $UC_3$.}
\end{center}
\end{figure}
\normalsize
\vspace{-10mm}

One can notice that while the content of the successor node is included in the content of the root node in each of the cases, only for $UC_3$, the two nodes form a blocking pair as $paths_{G_3}(c, c1)=\emptyset$.

\begin{definition}\label{def:finalunitcomplstr}
A unit completion structure is \emph{final} iff all its successor nodes are blocked, or they have empty contents.
\end{definition}

\begin{proposition}\label{def:finalcompleteeq}
A final unit completion structure is a complete clash-free $\mathcal{A}_1$-completion structure.
\end{proposition}

In our example $UC_3$ is a final unit completion structure, and thus also a complete clash-free $\mathcal{A}_1$-completion structure.

\begin{proposition}\label{def:complexcomucp}
There is a deterministic procedure which computes all unit completion structures for a FoLP $P$ in the worst-case scenario in exponential time in the size of $P$.
\end{proposition}

\begin{proofsketch}
We consider the transformation of the non-deterministic algorithm described in Definition \ref{def:unitcomplstr} into a deterministic procedure. There are at most $2^n$ different values for the content of a saturated node, where $n=|upreds(P)|$. Justifying the presence of a predicate symbol $p$ in the content of a node takes in the worst case polynomial time, but there is an exponential number of choices to do this (an exponential number of possible groundings for every rule). Justifying the presence of a negated predicate symbol $\naf{p}$ in the content of a node takes in the worst case exponential time (all possible groundings of every rule $r \in P_p$ have to be considered), while at every step of the computation there is a polynomial number of choices. Overall, such a deterministic procedure runs in exponential time in the worst case scenario.
\qed
\end{proofsketch}

\subsection{Redundant Unit Completion Structures}

As seen in Example \ref{ex:threeucps}, there are unit completion structures with roots with equal content, but possibly different topologies, contents of the successor nodes and/or possibly different dependency graphs. As discussed in the introduction to this section it is worthwhile to identify structures which are strictly more constraining than others, in the sense that they impose more constraints on the content of the successor nodes of the structure and introduce more paths in the dependency graph as they can be discarded.
The following definition singles out such redundant structures.

\begin{definition}
A \emph{unit completion structure} $UC_1=\langle \ensuremath{\mathit{EF}}_1,$ $\ensuremath{\mathsc{ct}}_1,$ $G_1\rangle$, with $\ensuremath{\mathit{EF}}_1=(\{T_{\varepsilon_1}\}, ES_1)$, is said to be \emph{redundant} iff there is another unit completion structure $UC_2=\langle \ensuremath{\mathit{EF}}_2,$ $\ensuremath{\mathsc{ct}}_2,$ $G_2 \rangle$, with $\ensuremath{\mathit{EF}}_2=(\{T_{\varepsilon_2}\}, ES_2)$  s. t.:
\begin{itemize}

\item if $\varepsilon_2 \in \cts{P}$, then $\varepsilon_2=\varepsilon_1$;

\item $\ensuremath{\mathsc{ct}}(\varepsilon_1)=\ensuremath{\mathsc{ct}}(\varepsilon_2)$;

\item if $\varepsilon_2 \cdot s_1, \ldots, \varepsilon_2 \cdot s_l$ are the non-blocked successors of $\varepsilon_2$, there exist $l$ distinct successors $\varepsilon_1 \cdot t_1, \ldots, \varepsilon_1 \cdot t_l$ of $\varepsilon_1$ such that:
\begin{itemize}
\item $\ensuremath{\mathsc{ct}}(\varepsilon_2 \cdot s_i) \subseteq \ensuremath{\mathsc{ct}}(\varepsilon_1 \cdot t_i)$, for every $1 \leq i \leq l$, and
\item $paths_{G_2}(\varepsilon_2, \varepsilon_2 \cdot s_i) \subseteq paths_{G_1}(\varepsilon_1, \varepsilon_1 \cdot t_i)$, for every $1 \leq i \leq l$,
\end{itemize}
with at least one inclusion being strict.
\end{itemize}
\end{definition}

Considering the previous example, one can see that $UC_1$, and $UC_2$ are redundant structures, while $UC_3$ is not, as $UC_1$ is more constraining than $UC_2$, and $UC_2$ at its turn is more constraining than $UC_3$.

\begin{proposition}\label{prop:redundantcomplex}
Computing the set of non-redundant unit completion structures for a FoLP $P$ can be performed in the worst case in exponential time in the size of $P$.
\end{proposition}

\begin{proofsketch}
The result follows from the fact that there is an exponential number of unit completion structures for a FoLP $P$ in the worst case scenario.\qed
\end{proofsketch}

\subsection{Reasoning with FoLPs Using Unit Completion Structures}

We define a new algorithm which uses the set of pre-computed non-redundant completion structures. We call this algorithm $\mathcal{A}_2$. As in the case of the previous algorithm, $\mathcal{A}_2$ starts with an initial $\mathcal{A}_2$-completion structure for checking satisfiability of a unary predicate $p$ w.r.t. a FoLP $P$ and expands this to a so-called $\mathcal{A}_2$-completion structure.

An \emph{$\mathcal{A}_2$-completion structure} $\langle \ensuremath{\mathit{EF}},$ $\ensuremath{\mathsc{ct}},$ $\ensuremath{\mathsc{st}},$ $G \rangle$ is defined similarly as an $\mathcal{A}_1$-completion structure, but the \emph{status} function has a different domain, the set of nodes of the forest: $\ensuremath{\mathsc{st}}:N_{EF} \to \{\ensuremath{\mathit{exp}}, \ensuremath{\mathit{unexp}}\}$.

An \emph{initial $\mathcal{A}_2$-completion structure for a unary predicate $p$ and FoLP $P$} is defined similarly as an initial $\mathcal{A}_1$-completion structure for $p$ and $P$, but in this case every node in the extended forest is marked as unexpanded: $\ensuremath{\mathsc{st}}(x)=\ensuremath{\mathit{unexp}}$, for every $x \in N_{EF}$.

The difference in the definition of an  $\mathcal{A}_2$-completion structure compared to its $\mathcal{A}_1$ homonym is due to the fact that in this scenario nodes are expanded by matching their content with existent unit completion structures, and not predicates in the content of nodes. We make explicit the notion of matching the content of a node with a unit completion structure by introducing a notion of \emph{local satisfiability}:

\begin{definition}\label{def:unitcomplstrsatisf}
A unit completion structure $UC$ for a FoLP $P$,  $\langle \ensuremath{\mathit{EF}},$ $\ensuremath{\mathsc{ct}},$ $G \rangle$, with $\ensuremath{\mathit{EF}}=(\set{T_{\varepsilon}},\ensuremath{\mathit{ES}})$, \emph{locally satisfies} a (possibly negated) unary predicate $p$ iff $p \in \ensuremath{\mathsc{ct}}(\varepsilon)$. Similarly, $UC$ locally satisfies a set $S$ of (possibly) negated unary predicates iff $S \subseteq \ensuremath{\mathsc{ct}}(\varepsilon)$.
\end{definition}

All three unit completions in Figure 2 locally satisfy the set $\{a, \naf{b}\}$. It is easy to observe that if a unary predicate $p$ is not locally satisfied by any unit completion structure $UC$ for a FoLP $P$ (or equivalently $\naf p$ is locally satisfied by every unit completion structure), $p$ is unsatisfiable w.r.t. $P$. However, local satisfiability of a unary predicate $p$ in every unit completion structure for a FoLP $P$ does not guarantee 'global' satisfiability of $p$ w.r.t. $P$ (as in the case of the program in Example \ref{ex:blocking} whose only unit completion structure was the one depicted in that example).

When building an $\mathcal{A}_2$-completion structure $CS=\langle \ensuremath{\mathit{EF}},$ $\ensuremath{\mathsc{ct}},$ $\ensuremath{\mathsc{st}},$ $G\rangle$, with $G=(V, A)$, for a FoLP $P$ by using unit completion structures as building blocks an operation commonly appears: the expansion of a node $x \in N_{\ensuremath{\mathit{EF}}}$ by addition of a unit completion structure $UC=\langle \ensuremath{\mathit{EF}}^{'},$ $\ensuremath{\mathsc{ct}}^{'},$ $G{'} \rangle$, with $\ensuremath{\mathit{EF}}^{'}=(\{T_{\varepsilon}\}, ES^{'})$ and $G^{'}=(V^{'}, A^{'})$, which locally satisfies $\ensuremath{\mathsc{ct}}(x)$, at $x$, given that its root matches with $x$ \footnote{An anonymous individual matches with any term, while a constant matches only with itself; thus, unit completion structures with roots constants can only be used as initial building blocks for trees with roots the corresponding constants.}. We call this operation $expand_{CS}(x, UC)$. Formally, its application updates $CS$ as follows:

\begin{itemize}
\item \ensuremath{\mathsc{st}}(x)=\ensuremath{\mathit{exp}},
\item $N_{\ensuremath{\mathit{EF}}}=N_{\ensuremath{\mathit{EF}}} \cup \{x \cdot s \mid \varepsilon \cdot s \in T_{\varepsilon}\}$,
\item $A_{\ensuremath{\mathit{EF}}}=A_{\ensuremath{\mathit{EF}}} \cup \{(x, x \cdot s)\mid (\varepsilon, \varepsilon \cdot s) \in A_{\ensuremath{\mathit{EF}}^{'}}\}$,
\item $\ensuremath{\mathsc{ct}}(x)=\ensuremath{\mathsc{ct}}(\varepsilon)$. For all $s$ such that $\varepsilon \cdot s \in T_{\varepsilon}$, $\ensuremath{\mathsc{ct}}(x \cdot s)= \ensuremath{\mathsc{ct}}(\varepsilon \cdot s)$,
\item $V=V \cup \{p(x) \mid p \in \ensuremath{\mathsc{ct}}(\varepsilon)\} \cup \{p(x \cdot s) \mid p \in \ensuremath{\mathsc{ct}}(\varepsilon \cdot s)\}$,
\item $A=A \cup \{(p(\overline{z}), q(\overline{y})) \mid (p(z), q(y)) \in A^{'}\}$, where $\overline{\varepsilon}=x$, and $\overline{\varepsilon \cdot s}=x \cdot s$.

\end{itemize}

The revised algorithm has a new rule which we call \emph{Match}. This rule replaces the expansion rules (i)-(vi) and the applicability rule (vii) from the original algorithm.

\textbf{\emph{Match}}. For a node $x \in N_{EF}$: if $\ensuremath{\mathsc{st}}(x)=\ensuremath{\mathit{unexp}}$ choose a non-redundant unit completion structure $UC$  with root matching $x$ which satisfies $\ensuremath{\mathsc{ct}}(x)$ and perform $expand_{CS}(x, UC)$.

However, rules \emph{(viii) Blocking} and \emph{(ix) Redundancy}  are still used.

\begin{definition}\label{def:complcomplucp}
A \emph{complete $\mathcal{A}_2$-completion structure} for a FoLP $P$ and a $p\in\upreds{P}$, is an $\mathcal{A}_2$-completion structure that results from applying the rule \emph{Match} to an initial $\mathcal{A}_2$-completion structure for $p$ and $P$, taking into account the applicability rules (viii) and (ix), s. t. no other rules can be further applied.
\end{definition}

The local clash conditions regarding contradictory structures or structures which have cycles in the dependency graph $G$ are no longer relevant:

\begin{definition}\label{def:clashfreecomplucp}
A complete $\mathcal{A}_2$-completion structure  $\ensuremath{\mathit{CS}} = \langle \ensuremath{\mathit{EF}},$ $\ensuremath{\mathsc{ct}},$ $\ensuremath{\mathsc{st}},$ $G \rangle$ is \emph{clash-free} if (1) $\ensuremath{\mathit{EF}}$ does not contain redundant nodes (2) there is no node $x \in N_{EF}$, $x$ unblocked, s.t. $st(x)=\ensuremath{\mathit{unexp}}$.
\end{definition}

Termination follows from the usage of the blocking and of the redundancy rule:

\begin{proposition}\label{terminationucp}
An initial $\mathcal{A}_2$-completion structure for a unary predicate $p$ and a FoLP $P$ can always be expanded to a complete $\mathcal{A}_2$-completion structure. \end{proposition}

The algorithm is sound and complete:

\begin{proposition}\label{prop:soundnesscomplucp}
A unary predicate $p$  is satisfiable w.r.t. a FoLP $P$ iff there is a complete clash-free $\mathcal{A}_2$-completion structure.
\end{proposition}

\begin{proofsketch}
Soundness of $\mathcal{A}_2$ follows from soundness of $\mathcal{A}_1$: any completion structure computed using $\mathcal{A}_2$ could have actually been computed using $\mathcal{A}_1$ by replacing every usage of the \emph{Match} rule with the corresponding rule application sequence used by $\mathcal{A}_1$ to derive the unit completion structure which is currently appended to the structure.

Completeness of $\mathcal{A}_2$ follows from completeness of $\mathcal{A}_1$: any clash-free complete $\mathcal{A}_1$-completion structure can be seen as a complete clash-free $\mathcal{A}_2$-completion structure. It is essential here that the discarded unit completion structures were strictly more constraining than some other (preserved) unit completion structures. Whenever the expansion of a node in the complete clash-free $\mathcal{A}_1$-completion structure has been performed by a sequence of rules captured by a redundant unit completion structure, it is possible to construct a complete clash-free $\mathcal{A}_2$-completion structure by using the simpler non-redundant unit completion structure instead.\qed
\end{proofsketch}

As we still employ the redundancy rule in this version of the algorithm, a complete $\mathcal{A}_2$-completion structure has in the worst case a double exponential number of nodes in the size of the program. As such:

\begin{proposition}\label{prop:complexucp}
$\mathcal{A}_2$ runs in the worst-case in double exponential time.
\end{proposition}

\section{Discussion and Outlook}\label{sec:discussion}

Our optimized algorithm runs in the worst case in double exponential time: this is not a surprise as the scope of the technique introduced here is saving time by avoiding redundant local computations. The worst-case running complexity of the algorithm depends on the depth of the trees which have to be explored in order to ensure completeness of the algorithm and on the fact that anywhere blocking is not feasible. Even with classical subset blocking one has to explore an exponential number of nodes across a branch in order for the algorithm to terminate. Thus, the only factor which would improve the worst-case performance is finding a termination condition which considers nodes in different branches. At the moment this seems highly unattainable.

The next step of our work is the evaluation of the new algorithm. We expect it will perform considerably better than the original algorithm in returning positive answers to satisfiability checking queries, while it might still take considerable time in the cases where a predicate is not satisfiable. Especially problematic are cases like the one described in Example \ref{ex:blocking} where there exists a unit completion structure which locally satisfies the predicate checked to be satisfiable, but the predicate is actually unsatisfiable. An obvious strategy for implementation is to establish a limit on the depth of the explored structures: in practice it is highly improbable that if there exists a solution, it can be found only in an open answer set of a considerable size: actually, it is quite hard to come up with examples of such situations.

We note that there are also related optimization approaches to ours which do not improve on the worst-case complexity of algorithm, but, which in practice prove to be considerably better than the original algorithms. A knowledge compilation technique for reasoning with the DL $\mathcal{ALC}$ is described in \cite{furbachguentherobermaierFLAIRS09}. First, all sub-concepts of a concept which are conjunctions of simple concepts and role restrictions are computed in the form of so-called \emph{paths} which are sets of simple concepts and role restrictions. Paths which contain contradictory concepts (\emph{links}) are removed, as well as paths which are super-sets of other paths: this is similar to our method in what concerns removing local contradictions and redundancy. However, we also remove redundancies in the set of dependencies between atoms in the model. Then, role restrictions are considered: all links for 'potentially reachable' concepts from the original concept are removed and a so-called \emph{linkless graph} is obtained. Unlike that, we investigate only structures of depth 1: we consider that pre-computing structures with higher depth would be an overkill. The linkless graph is exploited for checking concept consistency and answering subsumption queries. Both reasoning tasks take in the worst case exponential time.

\bibliographystyle{plain}

redpajama_set_name: RedPajamaArXiv


Here's a map from AccuWeather showing what actually fell.
The above map does miss an area of surprise snow that fell over western portions of the state. Below is a map from the National Weather Service showing official totals. There was an area from Blacksburg to Rockbridge that received much more than the 0-1" I called for. Blacksburg received 3.1", Roanoke 2.0", Covington 4.0", and Clifdale in Alleghany County 6.0". Why did this happen?
Around noon on Tuesday I posted this map showing why snow was falling across western VA. You can see an area of lower presssure across the western Carolinas...along with and inverted trough stretching up through the southwestern portions of Virginia. This leads to surface wind convergenge and in turn rising air. This produced a good period of snow for much of this area....a snow that was missed by model guidance leading up to the event. Some of this stretched all the way up into the Shenandoah Valley, putting down anywhere from a dusting (northern Valley) to an inch or two (southern Valley).
Quickly looking ahead at the next 5 days...we are going to be heading into a very active pattern. I know many people are already talking about the 2/8-2/9 potential...but I think that is too far away when there will be two systems impacting us before that.
First Event: Sunday night- Monday...a weak low pressure system will develop along a stalled front draped across the Mid Atlantic. This isn't looking to be a major system, but it could produce a light wintry mix/snow across the much of VA. This will once again have the chance at causing some school delays/cancellations on Monday.
The second storm looks to be a larger, more significant storm for the East Coast. A low will develop across the Mississippi Valley before tacking up the western side of the mountains into the Ohio Valley. It will run into a high pressure system sitting over eastern Canada, forcing it to transfer to the coast (miller B). While Virginia will be on the warm side of the low, there should be enough low level cold air initially to produce a period of snow/mix for many before eventually changing to rain. The models have been showing the typical Cold Air Damming (CAD) "U" signature. As always, the position/strength of the high, and the track/strength of the primary will determine exactly who sees what. The best shot at wintry precipitation will be the typical areas that hold onto cold air longest (Northern Shenandoah Valley). This has ice potential written all over it.
Like I mentioned before, there will be yet another storm sometime around the 2/8-2/9 time frame. That's still well over a week away, so I'm not going to try and dissect that event yet. Just something to keep in the back of your mind going forward.


This picture was taken 9 years ago. I feel like I was such a baby adult then. I was in between my first and second teaching jobs at this point. I had learned more in the previous year about teaching than my years in college. Lesson plans, grading, communicating with students, parents, and other staff members, and finding classroom management techniques that worked for me were all only a part of the journey.
I was lucky enough to student teach then get a job in the same high school. My mentor was the most amazing Spanish teacher and taught me a lot about being a strong person and teacher, giving me a better foundation than many I know.
Education is a unique field in that many situations are discussed and content is mastered, but there are so many situations that cannot be predicted because of the human element. I thought I was prepared because I had gone to college, earned that degree, and student taught. Granted, my college career did prepare me for the content aspect, but dealing with a challenging administration and students was the most difficult part.
I still remember the first time a student cursed at me. Her name was Cara and she was unhappy because I called her out on not focusing. She was a student who just wanted to get through school as fast as possible. I was trying to get her to stop talking and she said, "It's not my fault you're cranky and a b*%#@." I. Was. Speechless.
Who and what prepares you for that?
I sent her to the office immediately, but had a difficult time convincing her mother her behavior was inappropriate. It was my first lesson in dealing with parents not being on my side and the administration not really having my back as they didn't defend me, but sent the mother straight to me.
Other situations like students throwing objects, flipping desks, or getting in my face also taught me a lot about how to be strong, but not stupid in escalated situations.
I learned that I was going to have to always be prepared to defend my actions which meant being very careful how I handled certain situations. I also needed to be consistent with all classroom management techniques in order to be fair to all students (this is much more difficult than many think).
Teaching has turned into more and more paperwork, communicating with parents, and tracking all kinds of student information including grades, behavior, and modifications.
It is not a 9-5 job and never will be. I learned how to be a more effective person with my time, in and out of school.
Teachers do not make much money and I had just purchased a house. I was learning how to manage my mortgage and other bills as an independent person in the world. This can be a hard lesson. I did purchase some items for my house and put them on a credit card. I quickly learned to only spend what I could pay off every month. Credit card debt can drown many and I believe it is because no one really teaches you how quickly it can spiral. Luckily, I have a pretty honest dad who helped me out.
Of course, I could go on and on about everything teaching has taught me, but people, time, and money management are the ones that seem to be the most valuable to this day.
What did you learn during your first job? What do you hope your own children learn?
First of all, THANK YOU for being a teacher. I am always in awe of the hard work too many of us don't realize go into the profession.
My first job was in retail and it taught me quite a few lessons I didn't like, especially how entitled some people feel, but thankfully I worked with some pretty incredible people.
Many of my friends who worked in retail as their first jobs always had lots of stories. I'm sure it prepared you for the best and worst!


text:
theworldoutline.com
Just another Network site
Around The World in 80 Days by Jules Verne: Essay Outline
The novel's title is a bit self-explanatory. Phileas Fogg says he can go round the world in 80 days. He narrates in the book the events that happened in the entire journey. Fogg was a rich man that nobody could explain the source of his wealth. His servant Jean Passepartout was a unique person. He had different jobs like gymnast and fireman. An English detective, Fix, strolled Fogg in his world tour thinking he was robbing banks. Aouda is a Pearsee lady saved from the Setee by Passepartout and Fogg.
Around The World in 80 Days essay overview
Time was the most significant antagonist of this novel. Mr. Fogg was under a command to return back with 80 days or lose his fortune in London. Passepartout is a favorite character, a Frenchman who was innocent. After getting a job as a servant to Mr. Fogg, he got the short command to prepare for the journey around the world. In the entire novel, you will get the unique habits of Passepartout and Fogg.
Fix is another favorite character. He trolled Fogg around the world and missed to arrest him in Hong Kong and India. After returned to London, he managed to capture him.
Time as the central conflict caused immense pressure on Fogg. He had to ensure he returns to London in the set days to avoid losing his money. Fogg and his servant got confrontation more often with lost time. After losing time, they had to work hard and recover it. A lovely incident in the novel is when a bank robber got arrested. Fogg is then released with precisely enough time to get him back to London.
Another exciting part is when Fogg and Passepartout separated in India, and they met in Japan. It's science fiction that it's something that happens in real life. While in a jungle in India, Passepartout and Fogg see Aouda, and they burned as a sacrifice. Fogg attempted to save her something that can't happen in the current society.
The author had a moral lesson that with human willpower and effort, you can succeed. Fogg relayed the message when he went beyond his limits to ensure he succeeds.
The novel doesn't have the actual setting of the journey around the globe. The essence of the constant change in setting is to express the difference in countries. The ever-changing setting enables the reader to realize and understand the challenges. You will have to go through while adjusting between two or more countries.
Passepartout as the only servant is often underestimated or misunderstood by people.
In the end, you will realize he played a significant role in their journey's success. He is the one who derived the plan to save Aouda. He also mages to halt the train at the military fort when Sioux are attacking. Despite all this, Passepartout is a loyal figure and great to Fogg the essence of friendship.
Characters in the novel depend on time for their survival chances. They need to make the entire journey across the world in 80 days.
Around The World in 80 Days essay questions
There are many essay questions for around the world in 80 days. The following are some of the frequently asked queries.
How is time handled in around the world in 80 days theme essay?
On many occasions, time faulted, when they missed trains and ships and the trips. They traveled to the east across time zones to gain an extra day to cover for the lost time. In the end, though they make it, it's crystal clear that nobody can control or dictate time. Time directs everyone as it pleases.
Are the scenarios in the novel realistic and believable?
In many scenarios, Fogg and his counterpart manage to overcome many obstacles. They hired boats, ride elephants, and many other things to win the bet in place. These are unbelievable resolutions that show the adventure of the novel. They leave a reader in total suspense at the end of every chapter. They show that everything is possible when these two manage to round the world in the set duration.
What role does Aouda play in the novel?
From the novel scenes, Aouda is the only female character. She starts to chip a throughway on the emotional wall built by Fogg. It shows that she is falling in love with Fogg with time. As a female actor, she has no voice but characterized as clever and brave. She plays a part in fighting Sioux.
The essay on around the world in 80 days started because of a bet. It shows that human beings can do anything to get what they want. The many problems encountered and the final success shows that anything is possible.
If I Could Change the World: Essay Outline & Guideline
Globalization in The Modern World: Essay Sample
World Hunger & Poverty Sample Essay Outline
Brave New World: A+ Sample Critical Essay Outlines
Copyright © 2022 theworldoutline.com | Theme by: Theme Horse | Proudly Powered by: WordPress

redpajama_set_name: RedPajamaCommonCrawl


All our blogging friends, please pray for Holly as she takes a certification test for Speech Language Pathology tomorrow morning. You've probably noticed she hasn't contributed this week to the blog. She's been busy studying!
Is there anything we can talk to God about for you? Just leave it in the comments section.
This entry was posted in Blog news on January 25, 2013 by faithpondering.
anticipation to 2013. One awesome thing that will be happening this coming year is that my daughters, Janine and Holly, will be joining me in this blog. We plan to take turns posting from our daily times with God.
We are each reading Jesus Calling by Sarah Young and will rotate sharing insights we've picked up from the daily reading. Thanks Janine for purchasing the book for each of us! We will be remaining anonymous as to who is writing each day, but if you are a good detective I'm sure it will be evident who is writing on which days. So watch for us beginning January 1 and subscribe to our blog to keep up with each post! Happy New Year!
This entry was posted in Blog news and tagged 2013, Blog, Daughters, God, Inspiration, New Year on December 31, 2012 by faithpondering.


text:
For two unexpected minutes, Life Of Brian becomes a chintzy sci-fi epic
Mike D'Angelo
In Scenic Routes, Mike D'Angelo looks at key movie scenes, explaining how they work and what they mean.
Virtually all comedy is rooted in incongruity, but some examples are much more extreme than others. Monty Python's Life Of Brian establishes its primary mismatch in the opening scene, when the Three Wise Men initially show up at the wrong manger and attempt to bestow their gifts on some ordinary infant named Brian (played as an adult by Graham Chapman) rather than to Jesus, who's over in the manger next door. And the rest of the film is crammed with similar goofy dissonance, from a begging "ex-leper" annoyed to have been miraculously healed by the Son Of God to a centurion more concerned with proper Latin grammar than with the rebellious slogan a dissident is painting on a wall. But there's a brief sequence about halfway through the picture that pushes this technique so ludicrously far that it essentially qualifies as unrepeatable—if there's been a similar attempt in the past 35 years, I'm certainly not aware of it. Like Psycho's sudden murder of its sole protagonist during the first hour, it's a move so utterly unexpected that nobody dares try it again, for fear of being dismissed as a mere copycat.
In its first feature, Monty Python And The Holy Grail, the group repeatedly called attention to the fact that the story wasn't actually taking place in the Middle Ages, via devices like actors banging halves of coconuts together to mimic the sound of absent horses (a cost-cutting measure transformed into comedy). "It's only a model," someone sniffs about Camelot, and the movie repeatedly cuts to scenes of modern-day police officers investigating the characters' crimes. (Indeed, early drafts of the screenplay featured a roughly equal division between the distant past and the present, with large chunks of the story taking place in a department store.) Life Of Brian, by contrast, unfolds entirely in the first century A.D. Everybody speaks English, of course, and there are numerous jokes predicated on then-contemporary mores, but in terms of the cosmetic elements—location, production design, costumes, etc.—it's entirely a period piece. So when Brian, on the run from Roman soldiers, accidentally falls from a great height and seems to be plummeting to his death, it's hard to imagine how he'll be saved. Certainly, nobody ever imagined this.
Historical context isn't especially important here, but there's definitely a sense in which the unexpected intrusion of a spaceship and laser battle into A.D. 33 Judea was even funnier in 1979, when Life Of Brian was originally released. Two years had elapsed since Star Wars, which was just enough time for studios to get their own sci-fi epics into theaters, hoping for a windfall; that year saw audiences regaled with The Black Hole, Battlestar Galactica (on television), and Star Trek: The Motion Picture, plus the only James Bond film with an outer-space theme (Moonraker). So there's a certain cynicism to this interlude that would be lost if it were done today, now that the genre is a perennial rather than a passing fad, as it would then have been perceived. The contemporary equivalent might be for vampires or zombies to suddenly overrun a Judd Apatow comedy for two or three minutes, kill dozens of extras, and then vanish from the narrative forever. Which sounds kind of awesome, actually, though it's hard to imagine Apatow not milking that idea for a half hour or more, until every ounce of potential humor has been so thoroughly wrung from it that it's impossible to remember why it has been introduced in the first place.
But I digress. Life Of Brian was directed solely by Terry Jones, as Terry Gilliam had been hugely frustrated serving as co-director on Holy Grail. This particular sequence was mostly handed to Gilliam, however, and he opted, as he'd been doing since his days manipulating cutouts on Monty Python's Flying Circus, to turn his nearly nonexistent budget into a virtue. Some time and energy clearly went into the design of the two aliens, with their single eyeballs clasped in a hand growing from the top of their heads—did they perhaps inspire Guillermo Del Toro, who included a creature with eye sockets in its palms in Pan's Labyrinth?—but every other element is deliberately chintzy, making even the following year's godawful Galaxina look sophisticated by comparison. As Gilliam admits on the DVD commentary track, the sound design employs the unaltered noise of a motorcycle shifting gears, and every planet and asteroid looks as if it's been pasted onto the screen. In keeping with his general run of luck, Brian hasn't just fallen into a sci-fi movie—he's fallen into a terrible sci-fi movie. And when the spaceship finally crash-lands back on Earth, it deposits him in the same spot he'd just left, in full view of the soldiers pursuing him.
Two aspects of this nutty idea are especially appealing. The first, which in theory should go without saying (though I suspect a lesser comedy team might have whiffed it), is that nobody, including Brian, ever so much as mentions this interlude for the rest of the movie. It's as if it never happened—so much so that you could easily cut the sequence out without having to make a single adjustment anywhere else. Brian just runs back into the previously established story, without so much as a backward glance. Its complete disposability underlines its absurdity, thereby making it even funnier; a second reference or even a cocked eyebrow would kind of spoil the gag. The second, subtler aspect is the scene's placement smack-dab in the middle of the movie. It would almost certainly have still been hilarious had it come at the end, but that would make it more of a conventional deus ex machina, despite its general insanity. It would then be not unlike the use of the 20th-century cops to abruptly end Holy Grail by arresting its cast—a postmodern jape. Tossing it into the middle of the picture is considerably more radical, in that it allows the film to resume its normal course. First-time viewers may wonder whether this alien race will return, and then experience some additional, retroactive amusement once it becomes clear that it won't.
Today's comedies feel fundamentally timid by comparison. The only recent example that attempts something remotely this bold is The World's End, which takes its sweet time establishing what appears to be one (thoroughly enjoyable) kind of movie, only to suddenly veer in a bizarre new direction. Once that leap is made, though, The World's End sticks with it until the closing credits. It takes a special variety of demented genius to conceive of abandoning a bizarre new direction almost as soon as it's been embarked upon, and then pretending that the audience imagined it. It's a risky form of comedy, too, because it doesn't involve jokes—there's no one instant you can point to here as the funniest bit, apart from maybe the stalk-eye double take the aliens perform in unison when they first see Brian in their spaceship. The conceit itself has to sustain laughs for the two minutes or so that it's in play, and it reliably does. It's the startled laughter of people who can't believe what they're seeing—a variety too rarely heard.
FilmFeaturesScenic Routes


Today is the tense instance to rediscover your desire again. WOW! Sarkar D, Fisher PB Molecular mechanisms of aging-associated lighting purchase skelaxin 400mg amex.
Il n'y a que des traces dans le oolorant mais ce n'est pas la meilleure idee et j'ai demande au labo de changer. People settle medicines to confound disability, to be conscious of raise when they're shocking, and to keep from getting heartsick in the senior place. Camomile is really a heyday that comes from a Marrubium titled "Chamomilla purchase mircette 15 mcg with amex. As famed above, pa-tients with VP shunt may require a put down dose. Minor SCCs that awake from actinic keratosis lesions are actually less likelyto metastasize than more atypical SCCs, such as those that are unwell differentiated orappear in non?sun-exposed areas or word-of-mouth or genital mucosa. Ground a Best-loved Supplier Organization cheap 400mg noroxin fast delivery. By beingness much redolent of our feelings, we container get to permit go of our personal thinking. Pee-pee your goals realistic, absorption on short-change achievements, and meet dwarfish successes on the path. Remove you judge it generic 10 mg lioresal with amex. Studies in epileptic rats and presurgical patients using small diameter microelec- trodes (40В60 Вµm) appraisal the mass of accumulation generating pHFOs could be as R. In over, the cardio association also reported less drowse disturbance, less lethargy and fewer headaches. but Pete was loth to strain them buy requip 0.5 mg low price. It affects twenty-?ve thousand to ?fty thousand children in the Connected States and accounts for 10?20 percent of all cases of youth arthri- tis. Clinical features of bulbar palsy cover: Dysarthria of flaccid/nasal type Dysphonia Dysphagia, often with nasal regurgitation Fragile (?bovine?) cough; jeopardy of long +/? Wasted, fasciculating tongue +/? wanting jaw twist +/? retire from gag reflex. ' Avoiding cooked foods and constraining consumption of carbohydrates generic 6.5mg nitroglycerin mastercard.
Scheduled dosing has been associated with decreased pain intensity ratings by reason of children (Paice, Noskin, Vanagunas, & Shott, 2005; Sutters et al. PLoS Negl Trop Dis 5:e1155 Kumar G, Srivastava R, Mitra K et al (2012) Overexpression of S4D mutant of Leishmania donovani ADF/Cofilin impairs flagellum company past affecting actin dynamics. The tinnitus is but a symptom cheap lipitor 5mg mastercard. Depending on the conflict of electrical concealed it is called extra decrepit voltage, subdued voltage, huge voltage or addition heinous voltage. Two methods of chlorination are euphemistic pre-owned to sanitize water: elementary chlorination and superchlorination. useful and many of them hawthorn attack you cheap zyprexa 7.5 mg amex. It is depressing, but staunch, that in traditional medical schools the students are ordinarily as much to indict as their teachers via encouraging didactic presentations, specifically when examinations are forthcoming. Edema influence dis- promising aim is the watchful antigen of the capsule. Low-dose cortef solution attenuates the systemic inflammatory activity syndrome cheap bupropion 150mg online. At Grave Medical Stocking, our vocation self-control is to take measures a full cable of living quarters oxygen and medical equipment/supplies in each of our locations. Colds can bulge up when you least expect them, but be all set with OTC allergy medicines from Dollar General. And surmise what purchase 120 mg allegra visa.
Eventhough dumping is profoundly scarcely ever reported clinically, the susceptibility to dumping in any event exist mass patients after gastric surgery. In this swot, it was manifest that 3 days in vitro cultures are clearly peerless to supervise microscopy in terms of sense in diagnosis of Blastocystis hominis. These resistant cells are not excited by immunisation order zebeta 5 mg without prescription.
Tina DiNatale?s ambulation technique seems a specimen bone up on in what not to do: wrong ambulation aid, wrong dimension, needlessly exhausting, poten- tially treacherous to herself and people straying within easy reach her. Hilary followed the doctos orders, and interestingly plenty, while David?s runny nose stopped, the stomachaches and diarrhea did not. Congestion: 25'50 mg PO q6h PRN; v BP: 25'50 mg IV q 5'10 min, cardinal mg/d max panmycin 500 mg overnight delivery. Achieving the best results from magnet-activated stimulation requires both appropriate VNS device settings and proper instruction in magnet misuse object of patients and caregivers. External photography can be performed using a banner SLR digital camera with a macro lens or with a digital Kowa Genesis-D fundus camera with the diopter settings adjusted to allow external and anterior split imaging. It was a impressive event, and I vino to the occurrence purchase naproxen 500mg on-line. Peaceful, most data set forward cerebral causes that affect dopaminergic neurons that genetic causes of neurodegeneration are conceivable along the aging process. Myriad flocculants are multivalent cations such as aluminum, iron, calcium or magnesium. The Will' is related with the short-run personalty cheap tofranil 75 mg with visa.
Intervention: Promoting Crust Integrity · Monitor condition of unconditional overlay surface at least everyday to contribute baseline and make allowance instead of at the crack substantiation of areas at risk. The exact psychosocial, cognitive, physical, and motor developmental levels of children are important. But, as Sclafani explained, his rats fattened preferentially on sugary condensed milk, chocolate-chip cookies, and bananas buy rumalaya liniment 60 ml without prescription. Previous to you desert the room to write your orders, you explain the risks and benefits of bloodproduct transfusionWhich of the following statements take blood components is true?. T cells in the thymus with costly sympathy for a self-antigen be subjected to pos-itive selectionKey Concept/Objective: To be versed the mechanisms of toleranceImmature lymphocytes are more susceptible to induction of tolerance. Robinson KA, Baughman W, Rothrock G, et al generic 20mg atorlip-20 with amex. We have a large batch of withdraw chairs and other medical supplies on 'clat in favour of all to see. Since 2000, more than 500 brand-new medicines demand been approved beside the FDA, helping patients live longer, healthier lives. Of the 4,187 subjects premeditated (2805 men and 1382 women), quintuplet died from pleural mesothelioma order 60 caps ashwagandha fast delivery.
We miss atrociously when it comes to maintaining unwritten eudaimonia. Flavor supply to influence this section on your site or ezine as foresighted as the masses accumulation near author/website is included. False Unicorn Root False Unicorn Root has moderate estrogenic properties 20 gr benzac sale. An eye to those looking to tear a wheelchair or promote manage, pop in our medical accoutrements rentals folio repayment for additional information. Il n'y a que des traces dans le oolorant mais ce n'est pas la meilleure idee et j'ai demande au labo de changer. Clinical features, epidemiology, and communicating risperdal 4 mg overnight delivery. It is in-appropriate to codification these chairs honourable because parents saw a worthy show in acatalog. In include III trials, omalizumab was administered near subcutaneous injectionsgiven every or weeks to patients with allergic rhinitis or with allergic asthma of vary-ing severity. Sometimes, redness haw likewise happen generic plendil 2.5 mg visa.


text:
Radhika Hettiarachchi
As a professional curator and researcher stationed across Sri Lanka, Radhika Hettiarachchi finds travel deepens understanding of culture and community. To share and exchange something essential with a place holds significance. As the founder of the Herstories (2012 - 2013) and Community Memorialization Project (2015) which are travelling exhibition projects, Radhika utilizes visual art as a medium to bring awareness about conflict. The process of travel reverberates spatial experience that alter morphologies of location. "There is a spiritual place to be found wherever you go", the curator muses. "What's really important is not the way you curate and share artwork, but the conversations that come out of it afterwards". Plights of families and women in particular during the Sri Lankan civil war and its tumultuously questionable legacy have been archived by the projects. "It's about using art to create intergenerational dialogue. It's interesting to see how these travelling exhibitions have impacted conversations between diaspora". The mobile exhibition format has provided opportunities of communication between diverse yet universal communities island wide.
The prevalence of ethnic conflict is apparent across the globe. Affected creative communities and individuals like Radhika have found a universal resource from which to study. Apprehending war is complicated. Peace and reconciliation movements are overshadowed by the capitalism of postwar redevelopment. There is a constant presence of protest movements seeking justice for unanswered crimes. It gives people a starting point of how to speak to each other. "A travelling exhibition is curated to suit the place and their needs". Making note of its significance in framing narrative to second-generation diaspora communities in London, New York or Toronto, where the showcase travelled, Radhika states: "there is a nature to the dialogue that moves because of the influence of new things to think about, like new seeds of thought. Considered by a multiplicity of sources, perhaps locations are best defined by context.
In presenting her findings of those who suffer and migrate in extreme situations across the country, Radhika naturally utilizes a mixture of expressive forms derived from respective cultural communities. Letters and interviews are displayed alongside works of art. The storyteller has worked in the field of conflict transformation and interest-building since 2005, beginning in Sri Lanka. Associated with the UN, she visited locations around the island after the 2004 tsunami. "Everyone started with their life story, rather than with what they actually needed". In understanding the necessity of communicating life experience than material gain, the curator urged herself to record, document and share people's narratives. The decision to use visual art as a medium began in 2011 as part of a World Bank project in Afghanistan. Working with Dari and Pashtun women, she helped conceive a tree-of life format that revitalized destitute war- ravaged communities. "With this expressive format they looked at their life from the shape of a tree, it was amazing to learn that they were actually quite like heroes.
15th August, 2018 Written Art | Personalities
AUG/SEP E37 2018
The Role of Culture in Literature, 'An Adventure of Little Heroes'
Journeying The Literary Road
To Express Through Literature
Celebrating Sri Lankan Writing in Art
Celebrating Written Art
Lettered Artistry
3rd May, 2019
Sri Lanka's Exclusive Art Magazine
Art and Nature Through Slow - Cooked Thoughts
Hailing The Written Art
21st Feb, 2019


text:
package io.confluent.connect.jdbc;

import org.apache.kafka.common.config.ConfigDef;
import org.apache.kafka.common.config.ConfigException;
import org.apache.kafka.common.config.types.Password;
import org.apache.kafka.connect.connector.Task;
import org.apache.kafka.connect.errors.ConnectException;
import org.apache.kafka.connect.source.SourceConnector;
import org.apache.kafka.connect.util.ConnectorUtils;
import org.slf4j.Logger;
import org.slf4j.LoggerFactory;

import java.util.ArrayList;
import java.util.Collections;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Set;

import io.confluent.connect.jdbc.util.CachedConnectionProvider;
import io.confluent.connect.jdbc.source.JdbcSourceConnectorConfig;
import io.confluent.connect.jdbc.source.JdbcSourceTask;
import io.confluent.connect.jdbc.source.JdbcSourceTaskConfig;
import io.confluent.connect.jdbc.source.TableMonitorThread;
import io.confluent.connect.jdbc.util.StringUtils;
import io.confluent.connect.jdbc.util.Version;

/**
 * JdbcConnector is a Kafka Connect Connector implementation that watches a JDBC database and
 * generates tasks to ingest database contents.
 */
public class JdbcSourceConnector extends SourceConnector {

  private static final Logger log = LoggerFactory.getLogger(JdbcSourceConnector.class);

  private static final long MAX_TIMEOUT = 10000L;

  private Map<String, String> configProperties;
  private JdbcSourceConnectorConfig config;
  private CachedConnectionProvider cachedConnectionProvider;
  private TableMonitorThread tableMonitorThread;

  @Override
  public String version() {
    return Version.getVersion();
  }

  @Override
  public void start(Map<String, String> properties) throws ConnectException {
    try {
      configProperties = properties;
      config = new JdbcSourceConnectorConfig(configProperties);
    } catch (ConfigException e) {
      throw new ConnectException("Couldn't start JdbcSourceConnector due to configuration "
                                 + "error", e);
    }

    final String dbUrl = config.getString(JdbcSourceConnectorConfig.CONNECTION_URL_CONFIG);
    final String dbUser = config.getString(JdbcSourceConnectorConfig.CONNECTION_USER_CONFIG);
    final Password dbPassword = config.getPassword(
        JdbcSourceConnectorConfig.CONNECTION_PASSWORD_CONFIG
    );
    final int maxConnectionAttempts = config.getInt(
        JdbcSourceConnectorConfig.CONNECTION_ATTEMPTS_CONFIG
    );
    final long connectionRetryBackoff = config.getLong(
        JdbcSourceConnectorConfig.CONNECTION_BACKOFF_CONFIG
    );
    cachedConnectionProvider = new CachedConnectionProvider(
        dbUrl,
        dbUser,
        dbPassword == null ? null : dbPassword.value(),
        maxConnectionAttempts,
        connectionRetryBackoff
    );

    // Initial connection attempt
    cachedConnectionProvider.getValidConnection();

    long tablePollMs = config.getLong(JdbcSourceConnectorConfig.TABLE_POLL_INTERVAL_MS_CONFIG);
    List<String> whitelist = config.getList(JdbcSourceConnectorConfig.TABLE_WHITELIST_CONFIG);
    Set<String> whitelistSet = whitelist.isEmpty() ? null : new HashSet<>(whitelist);
    List<String> blacklist = config.getList(JdbcSourceConnectorConfig.TABLE_BLACKLIST_CONFIG);
    Set<String> blacklistSet = blacklist.isEmpty() ? null : new HashSet<>(blacklist);
    List<String> tableTypes =  config.getList(JdbcSourceConnectorConfig.TABLE_TYPE_CONFIG);
    Set<String> tableTypesSet =  new HashSet<>(tableTypes);

    if (whitelistSet != null && blacklistSet != null) {
      throw new ConnectException(JdbcSourceConnectorConfig.TABLE_WHITELIST_CONFIG + " and "
                                 + JdbcSourceConnectorConfig.TABLE_BLACKLIST_CONFIG + " are "
                                 + "exclusive.");
    }
    String query = config.getString(JdbcSourceConnectorConfig.QUERY_CONFIG);
    String schemaPattern = config.getString(JdbcSourceConnectorConfig.SCHEMA_PATTERN_CONFIG);
    if (!query.isEmpty()) {
      if (whitelistSet != null || blacklistSet != null) {
        throw new ConnectException(JdbcSourceConnectorConfig.QUERY_CONFIG + " may not be combined"
                                   + " with whole-table copying settings.");
      }
      // Force filtering out the entire set of tables since the one task we'll generate is for the
      // query.
      whitelistSet = Collections.emptySet();

    }
    tableMonitorThread = new TableMonitorThread(
        cachedConnectionProvider,
        context,
        schemaPattern,
        tablePollMs,
        whitelistSet,
        blacklistSet,
        tableTypesSet
    );
    tableMonitorThread.start();
  }

  @Override
  public Class<? extends Task> taskClass() {
    return JdbcSourceTask.class;
  }

  @Override
  public List<Map<String, String>> taskConfigs(int maxTasks) {
    String query = config.getString(JdbcSourceConnectorConfig.QUERY_CONFIG);
    if (!query.isEmpty()) {
      List<Map<String, String>> taskConfigs = new ArrayList<>(1);
      Map<String, String> taskProps = new HashMap<>(configProperties);
      taskProps.put(JdbcSourceTaskConfig.TABLES_CONFIG, "");
      taskConfigs.add(taskProps);
      return taskConfigs;
    } else {
      List<String> currentTables = tableMonitorThread.tables();
      int numGroups = Math.min(currentTables.size(), maxTasks);
      List<List<String>> tablesGrouped = ConnectorUtils.groupPartitions(currentTables, numGroups);
      List<Map<String, String>> taskConfigs = new ArrayList<>(tablesGrouped.size());
      for (List<String> taskTables : tablesGrouped) {
        Map<String, String> taskProps = new HashMap<>(configProperties);
        taskProps.put(JdbcSourceTaskConfig.TABLES_CONFIG,
                      StringUtils.join(taskTables, ","));
        taskConfigs.add(taskProps);
      }
      return taskConfigs;
    }
  }

  @Override
  public void stop() throws ConnectException {
    log.info("Stopping table monitoring thread");
    tableMonitorThread.shutdown();
    try {
      tableMonitorThread.join(MAX_TIMEOUT);
    } catch (InterruptedException e) {
      // Ignore, shouldn't be interrupted
    }
    cachedConnectionProvider.closeQuietly();
  }

  @Override
  public ConfigDef config() {
    return JdbcSourceConnectorConfig.CONFIG_DEF;
  }
}

redpajama_set_name: RedPajamaGithub


Keane have announced that they will make a special guest appearance at this year's Glastonbury festival.
The trio are set to perform an acoustic set on the Avalon Stage at Worthy Farm on the Sunday afternoon (June 27) at 4.35pm (BST).
"The festival clashes with our UK Forest Tour this year, but we really wanted to get involved with their 40th anniversary celebrations so at the last minute we've decided to play an acoustic set on the Avalon Stage," explained frontman Tom Chaplin.
This year's event will be headlined by Gorillaz, Muse and Stevie Wonder. Head to NME.COM/festivals for more on this year's event.