%May 4, 2005, for ACM TOCL
%May 26, 2005, final version with .bbl embedded

\documentclass[acmtocl,acmnow]{acmtrans2m}

\newtheorem{theorem}{Theorem}[section]
\newtheorem{conjecture}[theorem]{Conjecture}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{lemma}[theorem]{Lemma}
\newdef{definition}[theorem]{Definition}
\newdef{remark}[theorem]{Remark}

\usepackage{times}
\usepackage{latexsym}
\usepackage{epsfig}

\usepackage{graphicx}
\usepackage{pstricks, pst-node, pst-tree}
\usepackage{amsmath}

\usepackage{comment}
 

%\newcommand{\qed}{\mbox{$\Box$}} 

\newenvironment{INproof}{\begin{trivlist} 
\item[]{\it Proof.\ }}{ %
\mbox{}\hfill\qed %$\INBox$ 
\end{trivlist}}

\newenvironment{INproofsketch}{\begin{trivlist} 
\item[]{\it Proof Sketch.\ }}{ %
\mbox{}\hfill\qed %$\INBox$ 
\end{trivlist}}



%%%%%%%%%%%%%%%% LaTeX definitions %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

%\newtheorem{proposition}[theorem]{Proposition} 
%\newtheorem{lemma}[theorem]{Lemma} 
\newtheorem{example}[theorem]{Example} 
\newtheorem{algorithm}{Algorithm}[section] 


%%%%%%%%%%%%%%%%%%%%%%% END of LaTeX definitions %%%%%%%%%%%%%%%%%%%%%%%%%%%% 

\newcommand{\Not}{{\sf not} \,}
\newcommand{\expand}{{\sf expand}}
\newcommand{\lookahead}{{\sf lookahead}}
\newcommand{\smodels}{{\sf smodels}}

\newcommand{\dri}{ {\;{\vdash}_d} \;} 

\newcommand{\var}{\varphi}
\newcommand{\D}{\:\: |\:\:}
\long\def\comment#1{}

\newcommand{\inm}{\mbox{in}}
%\newcommand{\ta}{\mbox{truck\_at}}
%\newcommand{\pa}{\mbox{package\_at}}
%\newcommand{\taol}{\mbox{truck\_at\_other\_location}}
%\newcommand{\paol}{\mbox{package\_at\_other\_location}}
\newcommand{\ta}{\mbox{ta}}
\newcommand{\pa}{\mbox{pa}}
\newcommand{\taol}{\mbox{taol}}
\newcommand{\paol}{\mbox{paol}}
\newcommand{\myalign}{&\hspace{-.4in}&}


%\newenvironment{proof}{{\bf Proof:}}{\rule{2mm}{2mm}\\ }

\markboth{Fangzhen Lin and Jia-Huai You}{Recycling Computed Answers in Rewrite Systems for Abduction}

\title{\Large Recycling Computed Answers in Rewrite Systems for Abduction}

            
\author{Fangzhen Lin\\
Hong Kong University of Science and Technology
\and
Jia-Huai You\\
University of Alberta}

            
\begin{abstract} 
In rule-based systems, goal-oriented computations 
correspond naturally to the possible 
ways that an observation may be explained.
In some applications, we need
to compute explanations for a series of observations with the same domain.
The question whether previously computed answers can be recycled arises. 
A yes answer could result in substantial savings of repeated computations.
For systems based on classical logic, the answer is {\em yes}.
For nonmonotonic systems however, one tends to believe 
that the answer should be {\em no}, since recycling is a form of adding information.
In this paper, we show that computed answers can always
be recycled, in a nontrivial way, 
for the class of rewrite procedures proposed earlier by the authors for logic programs with negation.
We present some experimental results on an encoding of the logistics domain.
\end{abstract}
            
\category{I.2.3}{ARTIFICIAL INTELLIGENCE}{Deduction and Theorem Proving}[Logic programming \and Nonmonotonic reasoning]

            
\terms{Logic Programming, Abduction} 
            
\keywords{Stable model semantics, partial stable model semantics, rewrite systems, recycling}
            
\begin{document}

\begin{bottomstuff} 
An extended abstract of parts of this paper appeared in the 
proceedings of IJCAI-03, Acapulco, Mexico.\newline
Author's address: F. Lin, flin@cs.ust.hk,
Department of Computer Science,
Hong Kong University of Science and Technology,
Clear Water Bay, Kowloon, Hong Kong. \newline
Jia-Huai You, you@cs.ualberta.ca,
Department of Computing Science,
University of Alberta,
Edmonton, Alberta, Canada T6G 2E8.
\end{bottomstuff}
            

\maketitle


\section{Introduction}
The question we shall address in this paper is the following. With 
a sound 
and complete procedure for abduction, 
suppose we have computed explanations (conveniently represented 
as a disjunction)
$Es = E_1 \vee ... \vee E_n$
for observation $q$. 
Suppose also that in the course of computing explanations for another observation $p$,
we run into $q$ again. Now, we may use the proofs $Es$ for $q$
without actually proving $q$ again.
The question is this: will the use (recycling) of the proofs $Es$ for $q$ 
in the proof for $p$ preserve the soundness and completeness of the procedure? 

In this paper, we answer this question positively, but in a nontrivial way, 
for the class of rewrite procedures 
proposed in \cite{linyou02} for abduction in logic programming under
the (partial) stable model semantics (\cite{g-l-88-long}, \cite{prz-90b}).
The main result is a theorem (Theorem~\ref{main-theorem}) that 
says recycling preserves the soundness and completeness.

The general idea of recycling is not new.
Recycling in systems 
based on classical logic is always possible, since 
inferences in these systems can be viewed as 
transforming a logic theory to a logically equivalent one.
In dynamic programming, it is the use of the answers 
for previously computed subgoals that reduces the computational complexity.
In some game playing programs, 
for example in the world champion checker 
program {\em Shinook} (www.cs.ualberta.ca/\verb#~#chinook),
the endgame database stores
the computed results for endgame situations which can be referenced 
in real-time efficiently.

However, the problem of recycling in a nonmonotonic proof system has rarely
been investigated. We note that recycling 
is to use previous proofs.
This differs from adding consequences. 
For example, it is known that the semantics based on
answer sets or (maximal) partial stable models \cite{dun-91}
do not possess the 
{\em cautious nonmonotonicity} property. 
That is, 
adding a consequence of a program
could gain additional models thus losing some consequences.
The following example is due to \cite{dix-91}: 
\begin{equation}
\label{intro}
P = \{a \leftarrow \Not b.  ~~~b \leftarrow c, \Not a. ~~~c \leftarrow a.\}
\end{equation}
$P$ has only one answer set,
$\{a,c\}$. Thus, $c$ is a consequence. When augmented with the rule
$c \leftarrow$, the program gains a second answer set, 
$\{b,c\}$, and loses $a$ as a consequence. 

Abduction in the framework of
logic programming has been studied extensively, and
a number of formalisms and top-down query answering procedures have been proposed 
\cite{consoleJLP91,dun-91,dun-95-1,ek89-long,k-m-90,k-k-t-95,k-m-90p,k-m-mJLP00,linyou02,s-i-91,satoh-92-long}.
The
class of rewrite procedures for abduction proposed in \cite{linyou02}
is based on the idea of {\em abduction as confluent and terminating rewriting}.
These systems are called {\em canonical systems} in the literature of rewrite 
systems \cite{dershowitz90}.
The confluence and termination properties guarantee that rewriting 
terminates at a unique normal form
independent of the order of rewriting.
Thus, each particular strategy of rewriting 
yields a rewrite procedure. It has been shown in \cite{linyou02} that
these rewrite procedures are sound and complete under the semantics based on
partial stable models for {\em brave reasoning}; i.e., a query is true 
in a partial stable model if and only there is a proof by such a 
rewrite procedure.
Brave reasoning is particularly well suited for the task of 
generating explanations in abduction. In this paper, we show that the 
soundness and completeness of these rewrite procedures can be preserved
when they are extended with rules that ``recycle'' previous results.


This paper is organized as follows.
The next section defines logic program semantics.
Section~\ref{review} reviews the rewriting framework.
Then 
in Section~\ref{result} we formulate 
rewrite systems with computed rules and prove that recycling preserves 
soundness and completeness. Section~\ref{abduction} extends this result
to rewrite systems with abduction. Recycling incurs overhead and sometimes
the overhead could be substantial. 
A good recycling strategy makes computed answers 
likely to be used in later computations. In Section~\ref{strategy} we 
propose such a strategy, and 
Section~\ref{experiments} reports some experimental results.

\section{Logic Program Semantics}
A rule is of the form 
$$a \leftarrow b_1, ..., b_m, \Not c_1, ..., \Not c_n.$$
where $a$, $b_i$ and $c_i$ are atoms of the underlying propositional
language ${\cal L}$. $\Not c_i$ are called {\em default negations}. \
A {\em literal} is an atom $\phi$ or its negation $\neg \phi$.
A {\em (normal) program} is a finite set of rules.

The {\em completion} of a program $P$, denoted $Comp(P)$,
is a set of equivalences:
for each atom $\phi \in {\cal L}$, 
if $\phi$ does not appear as the head of any rule in $P$,
$\phi \leftrightarrow F \in Comp(P)$; 
otherwise, $\phi \leftrightarrow B_1 \vee ... \vee B_n \in Comp(P)$
(with default negations replaced by the corresponding negative literals)
if there are exactly $n$ rules 
$\phi \leftarrow B_i \in P$ with 
$\phi$ as the head; and these are the only equivalences in $Comp(P)$.
We write $T$ for $B_i$ if $B_i$ is empty.
 
The rewriting system of \cite{linyou02} 
is sound and complete w.r.t.\
the partial stable model semantics \cite{prz-90b}.
A simple way to define partial stable models without even 
introducing 3-valued logic is by the so called {\em alternating fixpoints} \cite{y-y-95}. 
Let $P$
be a program and $S$ a set of default negations.
Define a function over sets $S$ of default negations: 
$F_P (S) = \{ \Not a \, |\, P \cup S \not \vdash a\}$. 
The relation $\vdash$ is the standard propositional derivation relation with
each default negation $\Not \phi$ being treated as a named atom $\Not\_\phi$.

A {\em partial stable model} $M$ is defined by 
a fixpoint of the function that applies $F_P$ twice, 
$F_P^2 (S) = S$, while satisfying $S \subseteq F_P (S)$, 
in the following way: 
for any atom $\xi$, $\neg \xi \in M$ if $\Not \xi \in S$,
$\xi \in M$ if $P \cup S \vdash \xi$, and $\xi$ is {\em undefined}
otherwise. 
An {\em answer set} $E$ (also called {\em stable model}) is defined by a fixpoint $S$ 
such that $F_P (S) = S$ and $E = \{\xi \in {\cal L} ~|~P \cup S \vdash \xi\}$.



\section{Goal Rewrite Systems}
\label{review}

In this section, we briefly review goal rewrite systems as formulated 
in \cite{linyou02}. 

A goal rewrite system 
is a rewrite system that consists of three types of rewrite rules:
(1)
Program rules from $Comp(P)$ for literal rewriting; 
(2)
Simplification rules to transform and simplify goals; and
(3)
Loop rules for handling loops. 

A {\em program rule} is a completed definition 
$\phi \leftrightarrow B_1 \vee \ldots \vee B_n \in Comp(P)$ used from 
left to right: 
$\phi$ can be rewritten to $B_1 \vee \ldots \vee B_n$, and 
$\neg \phi$ to $\neg B_1 \wedge \ldots \wedge \neg B_n$.
These are called {\em literal rewriting}.


A {\em goal}, also called a {\em goal formula},
is a formula which may involve $\neg$, $\vee$ and $\wedge$. 
A goal resulted from a literal rewriting from another goal is 
called a {\em derived goal}. Like a formula, a goal may be transformed 
to another goal without changing its semantics. This is carried out
by simplification rules. 

We assume that in all goals 
negation appears only in front of a literal.  
This can be achieved by simple transformations like those used for converting
a formula to clauses.
 
\subsection{Simplification rules}
\label{3.1}

The simplification rules constitute a nondeterministic transformation system
formulated with a mechanism 
of loop handling in mind, which
requires keeping track of 
literal sequences \( g_0, \ldots, g_n \) where
each $g_i$, $0 < i \le n$, is in the goal formula resulted from 
rewriting $g_{i-1}$. Two central mechanisms in
formalizing goal rewrite systems are {\em rewrite chains} and {\em contexts}.

\begin{itemize}
\item
\underline{\em Rewrite Chain:}
Suppose a literal $l$ is written by its definition 
$\phi \leftrightarrow \Phi$
where $l = \phi$ or $l = \neg \phi$. Then,
each literal $l'$ in the derived goal is generated in order to 
prove $l$. This ancestor-descendant relation is denoted 
$l \prec l'$.
A sequence $l_1 \prec \ldots \prec l_n$ is then 
called a {\em rewrite chain}, abbreviated as $l_1 \prec^+ l_n$.

\item
\underline{\em Context:}
A rewrite chain $g = g_0 \prec g_1 \prec \ldots \prec g_n = T$ 
records a set of literals $C = \{g_0, ..., g_{n-1}\}$
for proving $g$.
We will write 
$T(\{g_0, ..., g_{n-1}\})$ and call $C$ a {\em context}.
A context will also be used to maintain consistency:
if $g$ can be proved via a conjunction, 
all of the conjuncts need be proved with 
contexts that are non-conflicting with each other.
For simplicity, we assume that whenever $\neg F$ 
is generated, it is automatically
replaced by $T(C)$, where $C$ is the set of literals on the corresponding 
rewrite chain,
and $\neg T$ is automatically replaced by $F$.
\end{itemize}

Note that for any literal in a derived goal, the 
rewrite chain leading to it from a literal in the given goal 
is uniquely determined.  
As an example, suppose the completion of a program has the definitions: 
$a \leftrightarrow \neg b \wedge \neg c$
and $b \leftrightarrow q \vee \neg p$. Then, we get a rewrite sequence,
$$a \rightarrow \neg b \wedge \neg c \rightarrow \neg q \wedge p \wedge \neg c.$$
For the three literals in the last goal, we have the following 
rewrite chains from $a$:
$$
\begin{array}{ll}
a \prec \neg b \prec \neg q\\
a \prec \neg b \prec p\\
a \prec \neg c
\end{array}
$$

\vspace{.1in}
\noindent
{\bf Simplification Rules:} Let $\Phi$ and $\Phi_i$ be goal formulas, 
$C$ be a context, and $l$ a literal.


\begin{itemize}
\item [SR1.]
$F \vee \Phi \rightarrow \Phi$
\item [SR1']
$\Phi \vee F \rightarrow \Phi$ 
\item [SR2.]
$F \wedge \Phi \rightarrow F$
\item [SR2']
$\Phi \wedge F \rightarrow F$
\item [SR3.]
$T(C_1) \wedge T(C_2) \rightarrow T(C_1 \cup C_2)$~~~ if $C_1 \cup C_2$ is consistent
\item [SR4.]
$T(C_1) \wedge T(C_2) \rightarrow F~~~$ if $C_1 \cup C_2$ is inconsistent
\item [SR5.]
$\Phi_1 \wedge (\Phi_2 \vee \Phi_3) \rightarrow (\Phi_1 \wedge \Phi_2) \vee (\Phi_1 \wedge \Phi_3)$
\item [SR5'.]
$(\Phi_1 \vee \Phi_2) \wedge \Phi_3 \rightarrow (\Phi_1 \wedge \Phi_3) \vee (\Phi_2 \wedge \Phi_3)$ \mbox{}\hfill\qed 
\end{itemize}
For any goal formula, repeated applications of SR5 and SR5' 
transform it to a disjunctive normal form (DNF).

\subsection{Loop rules}
After a literal $l$ is rewritten, it is possible that at some later stage
either $l$ or $\neg l$ appears again in a goal on the same rewrite chain. 
Two rewrite rules are formulated to handle loops.

\begin{definition}
Let $S = l_1 \prec^+ l_n$ be a rewrite chain.

\begin{itemize}
\item
If $\neg l_1 = l_n$ or $l_1 = \neg l_n$, then $S$ is called an {\em odd loop}.
\item
If $l_1 = l_n$, then
\begin{itemize}
\item
$S$ is called {\em a positive loop} if $l_1$ and $l_n$ are both atoms and 
each literal on $l_1 \prec^+ l_n$ is also an atom;
\item
$S$ is called {\em a negative loop} if $l_1$ and $l_n$ are both negative literals and 
each literal on $l_1 \prec^+ l_n$ is also negative;
\item
Otherwise, $S$ is called an {\em even loop}. 
\end{itemize}
\end{itemize}
In all the cases above, $l_n$ is called a {\em loop literal}.
\end{definition}


\vspace{.1in}
\noindent
{\bf Loop Rules:}  Let $g_1 \prec^+ g_n$ be a rewrite chain.
\begin{itemize}
\item [LR1.]
$g_n \rightarrow F$\\
if $g_i \prec^+ g_n$, for some $1 \le i < n$,
is a positive loop or an odd loop.
\item [LR2.]
$g_n \rightarrow T(\{g_1, ..., g_n\})$\\
if $g_i \prec^+ g_n$, for some $1 \le i < n$,
is a negative loop or an even loop. 
\mbox{}\hfill\qed 
\end{itemize}

\subsection{Goal rewrite systems}

A {\em rewrite sequence} is a sequence of zero or 
more rewrite steps $Q_0 \rightarrow \ldots \rightarrow Q_{k}$,
denoted $Q_0 \rightarrow^* Q_k$, such that 
$Q_0$ is an initial goal,
and for each $0 \le i < k$, 
$Q_{i+1}$ is obtained from $Q_i$ by 
\begin{itemize}
\item
literal rewriting at a non-loop literal in $Q_i$,
or 
\item
applying a simplification rule to a subformula of $Q_i$, or
\item
applying a loop rule to a loop literal in $Q_i$.
\end{itemize}

\begin{definition}
A {\em goal rewrite system} for a program $P$ is a triple 
$\langle {\cal Q}_L, {\cal R}_P, \rightarrow\rangle$,
where ${\cal Q}_L$ is the set of all goals,
${\cal R}_P$ is a set of rewrite rules which 
consists of program rules from $Comp(P)$, 
the simplification rules and the loop rules, and   
$\rightarrow$ is the set of all rewrite sequences. 
\end{definition}

In \cite{linyou02}, it is shown that
goal rewrite 
systems are sound and complete w.r.t.\ the partial stable model semantics:


\begin{theorem}  
\label{sound-and-complete}
Let $P$ be a normal program and 
$\langle {\cal Q}_L, {\cal R}_P, \rightarrow \rangle$
a goal rewrite system.

\vspace{.1in}
\noindent
{\sf Soundness:} For any literal $g$ and any rewrite sequence
$g \rightarrow^* T(C_1) \vee \ldots \vee T(C_m)$, 
there exists a partial stable model
$M_i$ of $P$, for each $i \in [1..m]$,
such that $g \in C_i \subseteq M_i$.

\vspace{.1in}
\noindent
{\sf Completeness:} For any literal $g$ true in 
a partial stable model $M$ of $P$,
there exists a rewrite sequence
$g \rightarrow^* T(C_1) \vee \ldots \vee T(C_m)$
such that for some $i \in [1..m]$, $g \in C_i \subseteq M$.
\label{sound-complete}
\end{theorem}  




\section{Goal Rewrite Systems with Computed Rules}
\label{result}

We now consider how to recycle computation in these rewrite systems.
Notice that what we eventually want is a theory of recycling in abductive
goal rewrite systems. But it is best to study the basic case where there
are no abducibles first. As we shall see, just as abducible rewrite
systems are a direct extension of rewrite systems as we showed in \cite{linyou02}, recycling in abducible rewrite systems is a direct extension of 
recycling in rewrite systems.

We first illustrate recycling with two examples.

\begin{example}
Given a rewrite system $R^0$, suppose we have a rewrite sequence 
$~\neg q \rightarrow a \rightarrow a \rightarrow F$.
The failure is due to a positive loop on $a$. 
We may recycle
the computed answer by replacing the rewrite rule for $\neg q$ by 
the new rule, $\neg q \rightarrow F$. We thus get a new system, say 
$R^1$. Suppose in trying to prove $g$ we have
$$g \rightarrow a \rightarrow \neg q \rightarrow F$$
where the last step makes use of the computed answer for $\neg q$.
The question arises as whether this way of using previously computed results
guarantees the soundness and completeness.
Theorem~\ref{main-theorem} to be proved later in this paper answers this 
question positively.
To see it for this example,
assume we have the following, successful proof
in $R^0$
$$g \rightarrow a \rightarrow \neg q \rightarrow a \rightarrow T(\{g,a,\neg q\})$$
where the termination is due the even loop on $a$.
Had such a sequence existed, recycling would have produced a wrong result.
However, one can see that the existence of the rewrite step 
$a \rightarrow \neg q$ implies the existence of a different way to
prove $\neg q$:  
$$\neg q \rightarrow a \rightarrow \neg q \vee \ldots \rightarrow T(\{\neg q, a\}) \vee \ldots$$
contradicting that $\neg q$ was rewritten to $F$ in $R^0$. \mbox{}\hfill\qed 
\end{example}

Before giving the next example, we introduce 
a different way to understand rewrite sequences. Since
any goal formula 
can always be transformed to a DNF using the distributive rules SR5 and 
SR5',
and the order of 
rewriting does not matter, we can view 
rewriting as generating 
a sequence of DNFs. Thus,
a rewrite sequence in DNF from 
an initial goal $g$,  
$$g \rightarrow^* N_1 \vee ... \vee N_n$$
can be 
conveniently represented by {\em derivation trees},
or {\em d-trees}, one for each $N_i$ representing one possible way
of proving $g$.
For any $i$, the d-tree for $N_i$
has $g$ as its root node, wherein a branch from $g$ to a leaf node 
corresponds to a rewrite chain 
from $g$ that eventually ends with an $F$ or some $T(C)$. 
As $N_i$ is a conjunction, a successful proof requires 
each branch to succeed (i.e. ends with $T(C)$ for some $C$)
and the union of all resulting contexts to be consistent. 

The next example is carefully constructed to illustrate that 
recycling may not yield the same answers as if no recycling were carried out. In particular, one can sometimes get additional answers.

\begin{example}
\label{main-example}
Consider the program:
\begin{eqnarray*}
\myalign g \leftarrow a.\ \ \ a \leftarrow \Not b.\ \ \ a \leftarrow e.\\ 
\myalign b \leftarrow b.\ \ \ e \leftarrow p. \ \ \ \ \ p \leftarrow a. \\
\end{eqnarray*}
\begin{figure}
\hspace{.25in}            
\pstree[nodesep=2pt,levelsep=20pt] {\TR{$p$}}
          {\pstree{\TR{$a$}} 
             {\pstree{\TR{$e$}} 
                {\pstree{\TR{$p$}} 
                   {\pstree{\TR{$F$}} 
                  {}}
                {}}
             {}}
}

\vspace{-1.42in}
\hspace{.87in}
\pstree[nodesep=2pt,levelsep=20pt] {\TR{$p$}}
          {\pstree{\TR{$a$}} 
             {\pstree{\TR{$\neg b$}} 
                {\pstree{\TR{$\neg b$}} 
                   {\pstree{\TR{$T(\{p,a,\neg b\})$}} 
                   {}}
                {}}
             {}}
}

\vspace{-1.4in}
\hspace{2.15in}
\pstree[nodesep=2pt,levelsep=20pt] {\TR{$g$}}
          {\pstree{\TR{$a$}} 
             {\pstree{\TR{$e $}} 
                {\pstree{\TR{$p$}} 
                    {\pstree{\TR{$a$}} 
                        {\pstree{\TR{$F$}} 
                        {}}
                    {}}
                {}}
             {}}
}


\vspace{-1.7in}
\hspace{2.9in} 
\pstree[nodesep=2pt,levelsep=20pt] {\TR{$g$}}
          {\pstree{\TR{$a$}} 
             {\pstree{\TR{$\neg b$}} 
                {\pstree{\TR{$\neg b$}} 
                  {\pstree{\TR{$T(\{g,a,\neg b\})$}} 
                  {}}
                {}}
             {}}
}


\vspace{-1.4in}
\hspace{3.9in}
\pstree[nodesep=2pt,levelsep=20pt] {\TR{$g$}}
          {\pstree{\TR{$a$}} 
             {\pstree{\TR{$e $}} 
                {\pstree{\TR{$p$}} 
                    {\pstree{\TR{$T(\{g,a,e,p,\neg b\}$)} }
                    {}}
                {}}
             {}}
}
\caption{Recycling may generate extra proofs}
\label{cross-over}
\end{figure}
In Fig.~\ref{cross-over}, each d-tree consists of a single branch.
The left two d-trees are expanded from goal $p$,
corresponding to the following rewrite sequence:
$$
\begin{array}{ll}
p \rightarrow a \rightarrow e \vee \neg b \rightarrow p \vee \neg b \rightarrow F \vee \neg b
\rightarrow \neg b \rightarrow \neg b \rightarrow T(\{p,a,\neg b\})
\end{array}
$$
The next two d-trees are generated for goal $g$,
corresponding to the rewrite sequence:
$$
\begin{array}{ll}
g \rightarrow a\rightarrow e \vee \neg b \rightarrow p \vee \neg b \rightarrow a \vee \neg b 
\rightarrow F \vee \neg b \rightarrow \neg b \rightarrow \neg b \rightarrow T(\{g,a,\neg b\})
\end{array}
$$
Now, we recycle the proof for $p$ in the proof for $g$ 
and compare it with the one without recycling.
Clearly, the successful d-tree for $g$ (the fourth from the left) will still succeed as it doesn't involve any $p$. 
The focus is then on the d-tree in the middle,
in particular, the node $p$ in it; this d-tree 
fails when no recycling was
performed.

 
Since $p$ is previously proved with context $\{g,a,\neg b\}$, 
recycling of this proof amounts to terminating $p$ with a context which is the union
of this context with the rewrite chain leading to $p$ (see the d-tree on the right).
But this results in a successful proof that fails without recycling. 

Though recycling appears to have generated a wrong result,
one can verify that both generated contexts,
$\{g,a,\neg b\}$ and $\{g,a,e,p,\neg b\}$,
belong to the same 
partial stable model. 
Thus, recycling
in this example didn't lead to an incorrect answer but generated
a redundant one.
Theorem~\ref{main-theorem}
shows that this is not incidental. 
Indeed, if $p$ is true in a partial stable model, by derivation (look at the d-tree
in the middle), so must be $e$, $a$, and $g$.  \mbox{}\hfill\qed 
\end{example}



\subsection{Rewrite systems with computed rules}
\label{4.1}

Given a goal rewrite system $R$, 
we may denote a rewrite sequence from
a literal $g$ by $g \rightarrow_R E$.
\begin{definition} {\rm (Computed rule)}\\
Let $R$ be a goal rewrite system in which literal $p$ is rewritten to
its normal form. The {\em computed rule for $p$} is defined as:
If $p \rightarrow_R F$, the computed rule for $p$ 
is the rewrite 
rule $p \rightarrow F$; 
if $p \rightarrow_R T(C_1) \vee ...\vee T(C_n)$,
then the computed rule for $p$ is the rewrite 
rule $p \rightarrow T(C_1) \vee ...\vee T(C_{n})$.
\end{definition}

For the purpose of recycling, a computed rule $p \rightarrow E$ 
is meant to replace the existing literal rewrite rule for $p$. 
If $E$ is $F$, i.e. the goal $p$ failed, then
it can be 
used directly as the literal rewrite rule for $p$.
Otherwise, we must combine the contexts in $E$ with the rewrite chain leading
to $p$, and keep only consistent ones. 

\vspace{.1in}
\noindent
\underline{\bf Recycling Rule:}  \\
Let $g_1 \prec^+ g_n$ be a rewrite chain where $g_n$ is a non-loop literal.
Let $G = \{g_1,...,g_n\}$, and 
$g_n \rightarrow T(D_1) \vee ... \vee T(D_k)$ be the computed rule for 
$g_n$. Further, let $\{D'_1,...,D'_{k'}\}$ be the subset 
of $\{D_1,...,D_k\}$ containing any $D_i$ such that 
$D_i \cup G$ is consistent.
Then, the {\em recycling rule} for $g_n$
is defined as:

\begin{itemize}
\item [RC.]
$g_n \rightarrow T(G \cup D'_1) \vee ... \vee T(G \cup D'_{k'})$ \mbox{}\hfill\qed 
\end{itemize}


\begin{example}
Consider the following program:
\begin{eqnarray*}
\myalign g \leftarrow a. ~~~~~~~~~~a \leftarrow p.\ \ \ ~~~~~~~p \leftarrow \Not a.\\ 
\myalign a \leftarrow \Not p.\ \ ~~ p \leftarrow \Not b. \ \ \ \ \ b \leftarrow \Not a. 
\end{eqnarray*}
and the proof:
$$
\begin{array}{ll}
p \rightarrow \neg a \vee \neg b \rightarrow p \vee \neg b \rightarrow
T(\{p,\neg a\}) \vee \neg b \\
\rightarrow
T(\{p,\neg a\}) \vee p \rightarrow T(\{p,\neg a\}) \vee T(\{p,\neg b\})
\end{array}
$$ 
We therefore have a computed rule for $p$:
$$p \rightarrow T(\{p,\neg a\}) \vee T(\{p,\neg b\})$$
Now, in the course of proving $g$ we can recycle the computed rule for $p$:
$$
\begin{array}{ll}
g \rightarrow a \rightarrow p \vee \neg p \rightarrow T(\{g,a, p,\neg b\}) \vee \neg p 
\rightarrow ...
\end{array}
$$
\end{example}


In the sequel, a rewrite system includes 
the recycling rule as well as zero or more 
computed rules. We note that 
the termination and confluence properties remain to hold
for the extended systems. 


We are interested in the soundness and completeness of 
a series of rewrite systems, each of which  
recycles computed answers generated on the previous one.
For this purpose, given a program $P$ we use $R_P^0$ to denote the 
original goal rewrite system where literal rewrite rules
are defined by the Clark completion of $P$. 
For all $i \ge 0$,
$R_P^{i+1}$ is defined in terms of $R_P^i$ as follows:
Let $\Delta_i$ be the set of computed rules 
(generated) on $R_P^i$ for the set of literals ${\cal L}_{\Delta_i}$
Then, $R_P^{i+1}$ is the rewrite system obtained from 
$R_P^i$ by replacing the rewrite rules for the literals in ${\cal L}_{\Delta_i}$ by those in $\Delta_i$. In the rest of this section,
we will always refer to a fixed program $P$. Thus we may drop the subscript $P$ and write $R^i$. 

\begin{definition}
A rewrite system $R^i$ is {\em sound} iff,  
for any literal $g$ and rewrite sequence 
$g \rightarrow_{R^i} T(C_1) \vee ... \vee T(C_n)$, 
and for each $C_j$, $j \in [1..n]$, 
there exists a partial 
stable model $M$ of $P$ such that $g \in C_j \subseteq M$.
$R^i$ is {\em complete} iff, for any literal $g$ such that
$g \in M$ for some partial stable model $M$ of $P$, there is a rewrite
sequence 
$g \rightarrow_{R^i} T(C_1) \vee ... \vee T(C_n)$ such that for some
$C_j$, $j \in [1..n]$, $g \in C_j \subseteq M$.
\end{definition}

An important property of provability by rewriting 
is the so-called {\em loop rotation}, which is needed in order to prove
the soundness and completeness of recycling; 
namely, a proof (a successful branch 
in a d-tree) terminated by a loop rule can be captured in rotated forms.

To describe this property, we need the following notation about rewrite chains:
Any direct dependency relation $l \prec l'$ may be 
denoted by $l \cdot l'$, and we allow a segment (which may be empty) 
of a rewrite chain to be denoted 
by a Greek letter such as $\delta$, $\theta$, and $\xi$.
Thus, we may write
$x \cdot \delta \cdot y$ to denote a rewrite chain from $x$ to $y$ via $\delta$,
and $x \cdot \delta$ 
to mean a rewrite chain that begins with $x$ followed by the segment 
denoted by $\delta$. 
A rewrite chain may also be used to denote the set of the literals 
on it.


\begin{lemma} (Loop rotation)\\
Let $R^0$ be a rewrite system without computed rules.
Let $Tr$ be a d-tree for literal $g$ that succeeds with context $C$.
Suppose a branch of $Tr$ ends with a loop, $g \cdot \theta \cdot g$, for
some $\theta$. 
Then, for any literal $l \in \theta$, there is a proof 
of $l$ that succeeds with the same context $C$.
\end{lemma}
\begin{INproof}
A loop, $\pi = g \cdot l_1 \cdot l_2 \cdot \ldots \cdot  l_n \cdot g$, 
where $g$ and $l_i$ are literals,
can always be rotated as 
$$
\begin{array}{ll}
l_1 \cdot l_2 \cdot \ldots \cdot l_n \cdot g \cdot l_1,\ \ \ \ \ \\
l_2 \cdot \ldots \cdot l_n \cdot g \cdot l_1 \cdot l_2,\ \ \ \ \\......
\end{array}
$$
and so on,
so that if $\pi$ is a negative loop (or an even loop, resp.) so is its
rotated loop. Rotation over a d-tree can be performed 
as follows: remove the top node $n$,
and for any link from the top node, $n \cdot q$, attach the link $n \cdot q$ 
to any occurrence of $n$. The assumption of the existence of 
loop $g \cdot \theta \cdot g$ ensures that 
in every round of rotation there is 
at least one occurrence of the top node. (See Fig.~\ref{rotation} 
for an illustration where rotation proceeds from left to right.)
It can be seen that the type of a loop is always preserved and the set of 
literals on the tree remains unchanged. 
\label{rotation-lemma}
\end{INproof}


\begin{figure}
\hspace{.3in}            
\pstree[nodesep=2pt,levelsep=20pt] {\TR{$g$}}
  {\pstree{\TR{$\neg b$}} 
          {\pstree{\TR{$a$}} 
               {\TR{$g$}
                \TR{$\neg b$}
               }
           \pstree{\TR{$\neg b$}}  
           {}
          }
  }

\vspace{-0.9in}
\hspace{1.9in}
\pstree[nodesep=2pt,levelsep=20pt] {\TR{$\neg b$}}
  {\pstree{\TR{$a$}} 
     {\pstree{\TR{$g$}} {\TR{$\neg b$}} 
      \pstree{\TR{$\neg b$}} 
      {}
     }
   \TR{$\neg b$} 
  {}
  }


\vspace{-0.9in}
\hspace{3.4in}
\pstree[nodesep=2pt,levelsep=20pt] {\TR{$a$}}
  {\pstree{\TR{$g$}} 
     {\pstree{\TR{$\neg b$}} 
       {\TR{$a$} \TR{$\neg b$}} 
     }
   \pstree{\TR{$\neg b$}}
       {\TR{$a$} \TR{$\neg b$}} 
  {}
  }


\caption{Loop rotation}
\label{rotation}
\end{figure}





\subsection{Soundness and completeness of recycling}

Below, given a literal $l$, by {\em a proof of $l$} we mean a
rewrite sequence from $l$ to 
$T(C_1) \vee \ldots \vee T(C_n)$,
where any $C_i$ can be referred to as a proof of $l$.

\begin{theorem}
\label{main-theorem}
For any $i \ge 0$, $R^i$ is sound and complete.
\end{theorem}

\begin{INproof} 
We prove the claim by induction on $i$. 
$R^0$, the system without computed rules, 
is sound and complete \cite{linyou02}.
Now assume for all $j$ with $0 \le j \le i$, $R^j$ are sound and complete, and show that 
$R^{i+1}$ is also sound and complete.

We only need to consider the situations where rewriting in $R^{i+1}$ 
differs from that of $R^i$. 
Let ${\cal L}_{\Delta_i}$ be the set of literals whose computed rules are generated on $R^i$.
We can first carry out rewriting
without rewriting the literals that are 
in ${\cal L}_{\Delta_i}$. In this case, 
rewriting from $g$ in both $R^i$ and $R^{i+1}$ 
terminate at the same expression, which is either $F$ or a DNF, say
$N_1 \vee... \vee N_m$. Each $N_i$ can be represented
by a d-tree.

\vspace{.1in}
\noindent
{\em Soundness:} 
Suppose $g \rightarrow_{R^{i+1}} T(D_1) \vee ... \vee T(D_s)$. For any 
$D \in \{D_1,...,D_s\}$ we need to show that there is a partial stable 
model $M$ such that $D \subseteq M$.
Consider the d-tree $Tr$ that generates $D$ and suppose $g$ is
its root node.
We show inductively in a bottom-up fashion that all the literals on 
$Tr$ must be in the same partial stable model. 
For any leaf node $p$
that is terminated by its computed rule 
$$p \rightarrow ... \vee T(C) \vee...$$
suppose $Tr$ is the one
that succeeded with context $C$.
By the inductive hypothesis on $R^j$,
we know that $R^j$ is sound for all $j \le i$,
thus there is a partial stable model $M$ such that $C \subseteq D \subseteq M$.
If a leaf node $q$ is terminated by a loop, by the loop rotation lemma
(lemma~\ref{rotation-lemma}), there is a proof of $q$ in $R^i$ 
using rotated loops. Otherwise we have an obvious case where
a leaf node is rewritten to $True$ by its Clark completion.

In the inductive step, let $l_1,...,l_n$ be the child nodes of some node $l$ 
and assume each $l_i$ is proved in $R^i$ hence in some partial stable model. 
We first show that they belong to the same partial stable model $M$. Then,
we show that $l$ can also be proved in $R^i$ thus belonging to $M$ 
as well.
Without loss of generality, assume
there are only two child nodes:
$l_1 \rightarrow_{R^i} T(Q_1) \vee ... \vee T(Q_m)$, 
$l_2 \rightarrow_{R^i} T(W_1) \vee ... \vee T(W_n)$.
Since $D$ is constructed in $R^{i+1}$ using computed rules, by definitions
of computed rule and the recycling rule,
there are $Q_i$ and $W_j$ such that
$Q_i \cup W_j \subseteq D$, and hence $Q_i \cup W_j$ is consistent.
Then in $R^i$, the two contexts are merged by using simplification rule SR3, i.e.,
$$l_1 \wedge l_2 \rightarrow_{R^i} ... \vee [T(Q_i) \wedge T(W_j)] \vee ...
\rightarrow_{R^i} ... \vee T(Q_i \cup W_j) \vee ...$$
Since $R^i$ is sound, there is a partial stable model $M$
such that $\{l_1,l_2\} \subseteq Q_i \cup W_j \subseteq M$.
But $l$ is derivable from $l_1$ and $l_2$. Using the definition of 
partial stable models, it can be shown 
that $l$ must also be in $M$.

The induction allows us to conclude that 
for the top goal $g$ and its proof $D$ in $R^{i+1}$, we must have 
$g \in D \subseteq M$, for the same partial stable model $M$.

\vspace{.1in}
\noindent
{\em Completeness:} 
We show that for any context generated in $R^i$, 
the same context will be generated in $R^{i+1}$. Then, 
$R^{i+1}$ is complete simply because $R^i$ is complete.

Let $p \in {\cal L}_{\Delta_i}$, and consider a proof of $g$ via $p$ and its
d-tree.
Since each branch of this d-tree can be expanded and eventually terminated 
independent of others, for simplicity, we consider a proof of $g$ simply by 
(an extension of) a branch $g \cdot \xi \cdot p$.  
In $R^{i+1}$ the computed rule for $p$ is used while 
in $R^i$ it is not. 
We only need to consider two cases of proof in 
$R^i$: 
either $g$ is proved via $p$ and a previously computed rule, 
or the proof is terminated due to a loop.

\vspace{.1in}
\noindent
(i) The case of loops. In expanding the rewrite chain 
$g \cdot \xi \cdot p$ in $R^i$,
we may form a loop, say $g \cdot \xi \cdot p \cdot \xi'$. If the loop is in $\xi'$,
exactly the same loop occurs in rewriting $p$ as the top goal in $R^i$,
so it is part of the computed rule for $p$. Otherwise it is a
loop that {\em crosses over p}, in the general form
$$\pi = g \cdot \theta_1 \cdot l \cdot \theta_2 \cdot p \cdot \theta_3 \cdot l$$
where $l$ is the loop literal. As a special case of loop rotation over a branch
(cf. Lemma~\ref{rotation-lemma}),
the same way of 
terminating a rewrite chain presents itself in proving $p$ 
as the top goal in $R^i$, which is
$$\pi' = p \cdot \theta_3 \cdot l \cdot \theta_2 \cdot p.$$ If the loop on $\pi$ is a
negative loop (or an even loop, resp.), so is $\pi'$. 
Thus the same context will be generated in $R^{i+1}$.

\vspace{.1in}
\noindent
(ii) $g$ is proved via $p$ and a previously computed rule. That is, $R^i$
gives a rewrite chain of the form 
$g \cdot \xi \cdot p \cdot \delta \cdot q$ where $q \rightarrow E$ is a computed rule generated on $R^j$ for some $j < i$. 
Suppose the context generated this way
is $C$.
Because of the existence of $p \cdot \delta \cdot q$, exactly the same computed rule 
$q \rightarrow E$ must be used in generating the computed rule for $p$ in $R^i$.
It can be seen that the context generated in $R^{i+1}$
by recycling the computed answers for $p$ (which is computed via $q$)
is exactly the same as the one that uses the computed answers for
$q$ but not those for $p$.
So, for any context generated this way in $R^i$,
the same context will be generated in $R^{i+1}$ as well.
\end{INproof}



As given in the corollary below, if we only recycle failed proofs then exactly the same contexts will
be generated.
\begin{corollary}
\label{fail_case}
Let $R^i$ be a rewrite system where each computed rule is of the 
form $p \rightarrow F$. Let $g$ be a literal and $E$ be a normal form.
Then, for any $i \ge 0$,
$g \rightarrow_{R^0} E~~~\mbox{iff}~~~g \rightarrow_{R^i} E$.
\end{corollary}


\begin{INproof}
Let $\Delta$ be the set of literals whose rewrite rules are 
computed rules in $R^i$. By the condition in the corollary, each such
computed rule is of the form $p \rightarrow F$. 
First consider the process of rewriting goal $g$ to a normal
form $E$ in which each literal in $\Delta$ is treated as a terminal
node. Note that $E$ is a DNF, or a d-tree where some of the leaf nodes
are literals in $\Delta$.
Then, continue rewriting from $E$ in $R^0$ where each literal 
in $\Delta$ is eventually rewritten to $F$. Let the normal form be
$E'$.
Also continue rewriting from $E$ in $R^i$ where
each literal in $\Delta$ is replaced by $F$, and thus the eventual normal
form is exactly the same as $E'$.
\end{INproof}

\section{Recycling in Abductive Rewrite Systems}
\label{abduction}

So we have shown that recycling can be done rewrite systems 
that does not have any
abducibles. As we mentioned, this is just the base case. Our aim is to do recycling in
rewrite systems with abducibles. Without abducibles, the basic problem is
simply that, given a program $P$ and a goal $g$, decide if there is a stable model
that satisfies $g$. While
the rewrite framework
studied in this
paper may turn out to be a good way of solving this problem,
currently the best
approach to answer this question is to use a stable model
generator such as Smodels \cite{smodels} or ASSAT \cite{LinZhao:assat}.
However, when there are many abducibles, and the problem is to find
explanations of a goal in terms of these abducibles, then the rewrite
systems here are better than answer set generators, as we discussed at the
end of Section 7 in \cite{linyou02}.
In the following, we first review an abductive framework as given in
\cite{linyou02}, we then review how rewrite systems are extended to
handle abduction in \cite{linyou02}. Finally, we show how our results about
recycling in rewrite systems can be similarly extended to that in abducible
rewrite systems.

\subsection{An abductive logic programming framework}
\label{abduction0}

In the following, let $P$ be a normal logic program, and $A$ a set of
atoms called {\em abducibles}. We also assume
that abducibles do not occur
as the head of a rule. All the definitions and results below are
from \cite{linyou02}.

By
a {\em hypothesis} $\alpha$ we mean a consistent set of literals over
$A$, 
i.e.,
it is not the case that $p$ and $\neg p$ are both in $\alpha$ for some
$p\in A$.
We say that a hypothesis is {\em complete} if for each atom $p\in A$, 
either $p$ or $\neg p$
is in $\alpha$, but not both.
Notice that a complete hypothesis is really a truth-value assignment over
the language $A$.
We say that a hypothesis $\alpha$ is an {\em extension}
 of another one $\beta$ if
$\beta\subseteq\alpha$, and a complete extension if it is an extension that is
complete.

\begin{definition}
A complete hypothesis $\alpha$ is said to be an
explanation  of an atom $q$ w.r.t.\ $P$ and $A$ iff there is an answer set
$M$ of $P\cup \alpha^+$ 
such that $M$ contains $q$ and for any $\neg p\in \alpha$, $p\not\in M$, where
$\alpha^+$ is the set of atoms in $\alpha$. 
\end{definition}


\begin{definition}
A hypothesis is said to be
an explanation of $q$ iff every complete extension of it
is an explanation.
A hypothesis
$\alpha$ is said to be a minimal explanation if it is an explanation, and
there is no other explanation $\alpha'$ such that $\alpha'\subset \alpha$.
\end{definition}

Consider the following logic program $P$ 
\begin{eqnarray*}
&& canCross \leftarrow boat, \Not leaking.\\
&& canCross \leftarrow boat, leaking, hasBucket.
\end{eqnarray*}
about $canCross$.
The following are the complete hypotheses
that explain $canCross$:
\begin{eqnarray*}
\hspace*{-2em} &&
\{ boat, \neg leaking, \neg hasBucket\},\\
\hspace*{-2em} &&
\{ boat, \neg leaking, hasBucket\},
\{ boat, leaking,  hasBucket\}.
\end{eqnarray*}
Now consider $\{ boat, hasBucket\}$. Clearly every complete extension of this
set is an explanation, so it is an explanation as well.
Furthermore, it is a minimal explanation as none of its element can be
deleted for it continue to be an explanation. 
Similarly, $\{ boat, \neg leaking\}$
is also a minimal explanation.

If we take a hypothesis to be the conjunction of its elements,
then we have that in propositional logic,
\[
\bigvee_{\alpha\in {\cal S}_1} \alpha \equiv 
\bigvee_{\alpha\in {\cal S}_2} \alpha 
 \equiv 
\bigvee_{\alpha\in {\cal S}_3} \alpha 
\]
where ${\cal S}_1$ is the set of all complete hypotheses that are
explanations of $q$, ${\cal S}_2$ the set of all explanations
of $q$,
and ${\cal S}_3$ the set of all 
minimal explanations of $q$.
Therefore the set of minimal explanations is a 
succinct representation of the set of all explanations.

Computationally, it may be hard to compute minimal explanations from
scratch. It is often easier to compute first a small ``cover'' of
all explanations.

\begin{definition}
A set $\cal S$ of hypotheses is said to be a {\em cover}
of $q$ w.r.t.\ $P$ and $A$ iff
\[
\bigvee_{\alpha\in {\cal S}} \alpha \equiv 
\bigvee_{\alpha\in {\cal S}_0} \alpha,
\]
where
${\cal S}_0$ is the set of minimal explanations of $q$. 
\end{definition}

\begin{proposition}
If $\cal S$ is a cover of $q$, then each $\alpha\in \cal S$ must be an
explanation of $q$.
\end{proposition}

So a cover is a set of explanations such that any complete explanation
must be an extension of one of the explanations in the cover.
Once we have a cover, then we can find all minimal explanations by
propositional reasoning alone:

\begin{proposition}
Let $\cal S$ be a cover of $q$. Then a hypothesis is
a minimal explanation of $q$ iff it is a prime implicant of
$\bigvee_{\alpha\in \cal S} \alpha$.
\end{proposition}

Finally a remark here about the relationship between our notion of explanations
and that of abductive explanations of Kakas and Mancarella's \cite{k-m-90}.
It can be shown that
a complete hypothesis $\alpha$ is an explanation of $q$ iff
$\alpha^+$ is an abductive explanation of $q$ according to
Kakas and Mancarella's definition. So what is new here is a notion of
minimal explanations. This is important as the number of complete
explanations can be significantly larger than the number of minimal
explanations. More importantly, minimal explanations capture a notion
of ``relevance'' that is not there in complete explanations. More
discussions about this can be found in \cite{linyou02}.


\subsection{Abductive Rewrite Systems}

Again, all results in this subsection are from \cite{linyou02}.
Firstly, as shown in \cite{linyou02}, the rewriting framework
can be extended to 
abduction in a straightforward way: the only difference in the extended 
framework is that we do not apply the Clark
completion to abducibles. 
That is,
once an abducible appears in
a goal, it will remain there unless it is eliminated by
the simplification rule $SR2$ or $SR2'$. In a similar way, the goal rewrite
systems with computed rules in the previous section can be extended to
abduction as well.

As an abducible may appear in a goal positively or negatively,
we need a terminology to refer to both of them:
an {\em abducible literal} is either an abducible $\phi$ or
its negative counterpart $\neg \phi$. 
Just like a rewrite to $T$ is written as $T(C)$, where $C$ is the underlying
rewrite chain (cf. Section~\ref{3.1}), a rewrite to an abducible literal 
$l$ will be written as $l(C)$ where $C$ is the rewrite chain leading
to, and including $l$. Thus when we write $l(C)$, it is understood
that $C$ always contains $l$.

In the following we shall denote by
$\langle {\cal Q}_L, {\cal R}_P, A, \rightarrow \rangle$ the rewrite system
obtained by the logic program $P$ and the set $A$ of abducibles. Recall that
${\cal Q}_L$ is the set of all goals.
The following theorem from \cite{linyou02} shows that these
 rewrite systems are both sound and complete with respect to 
the partial stable models semantics. 


\begin{theorem}  
\label{main2}
Let $P$ be a finite program, $A$ a set of abducibles, and
$\langle {\cal Q}_L, {\cal R}_P, A, \rightarrow \rangle$
the goal rewrite system with respect to $P$ and $A$.

\vspace{.1in}
\noindent
{\sf Soundness:} For any literal $g$ and any rewrite sequence
\[
g \rightarrow^* G \vee [l_1(C_1)\land\cdots\land l_k(C_k)] \vee G',\]
where each $l_i$ is either an abducible literal or $T$,
if $C_1\cup\cdots\cup C_k$ is consistent, then
there exists a partial stable model
$M$ of $P\cup \{l_1,...,l_k\}^+$
such that $g \in \bigcup_{1\leq j\leq k} C_i \subseteq M$.

\vspace{.1in}
\noindent
{\sf Completeness:} For any set of atoms $S\subseteq A$, and any
literal $g$ in 
a partial stable model $M$ of $P\cup S$,
there exists a rewrite sequence
\[
g \rightarrow^* G\vee [l_1(C_1)\land\cdots\land l_k(C_k)] \vee G',\]
such that
$g \in \bigcup_{1\leq j\leq k} C_j \subseteq M$.
\end{theorem}

Notice that our soundness and completeness result is stated with respect to
partial stable models, but our abductive framework in section~\ref{abduction}
is defined with the stable model semantics in mind. In general, a stable
model is also a partial stable model, but the converse is not always true.
Thus our rewrite systems may not be sound under the stable model semantics.
The reason is that stable models check for global
consistency, but our rewrite systems check only local ones.
There are several ways
to make the rewriting system also sound and complete for stable models.
One way is that when a conjunction of abducibles 
\[
l_1(C_1)\land\cdots\land l_k(C_k)\]
is generated, one can check if $C=C_1\cup\cdots\cup C_k$ is consistent
and complete. If it is, then $\{ l_1,...,l_k\}$ is an explanation. If
it is consistent but not complete, then we can either call a stable
model generator to see if $C$ can be extended to a stable model or we
can choose an atom $p$
such that neither it nor its negation is in $C$, and
continue the rewriting with either $p(C)$ or $\neg p(C)$, until a
complete context is obtained.

There is however an important special class of logic programs where
partial stable models and stable models coincide.
We say that a program has no odd loops (odd-loop free)
if there is no odd loop starting
with any literal. Since goal rewrite systems are confluent, any odd-loop in 
the program's dependency graph can replicate itself in a rewrite chain of 
some goal rewrite sequence. 
Therefore, there is no essential difference between 
our notion of odd-loop free and the notion of 
{\em negative cycle free} in the literature \cite{fages94,sato90}.

The following theorem is proved in \cite{linyou02}.

\begin{theorem}  
\label{main3}
Let $P$ be a finite program, and
$\langle {\cal Q}_L, {\cal R}_P, A, \rightarrow \rangle$
a goal rewrite system. 
Suppose $q$ is a proposition and
\begin{eqnarray*}
&& q \rightarrow^* [l_{11}(C_{11})\land\cdots\land l_{1k_{1}}(C_{1k_{1}})] \vee \ldots \vee\\
&&\hspace*{2em}  [l_{m1}(C_{m1})\land\cdots\land l_{mk_{m}}(C_{mk_{m}})]
\end{eqnarray*}
is a rewrite sequence such that each $l_{ij}$ is either $T$ or 
an abducible literal, and
$C_{i1}\cup\cdots\cup C_{ik_i}$ is consistent for each $i$.
If $P$ has no odd loops then
\[ \{
\{ l_{11},\cdots,l_{1k_{1}}\}, \cdots,
\{ l_{m1},\cdots,l_{mk_{m}}\} \}
\]
is a cover of $q$. In general, for arbitrary $P$ we have
\[ 
\bigvee_{\alpha\in \cal S}\alpha \supset
[l_{11}\land\cdots\land l_{1k_{1}}]\lor \cdots\lor
[l_{m1}\land\cdots\land l_{mk_{m}}]
\]
where $\cal S$ is any cover of $q$. 
\end{theorem}

\subsection{Recycling in Abductive Rewrite Systems}

We now show that 
recycling can be extended to abductive rewrite systems as well.


\begin{definition} {\rm (Computed rule for abduction)}\\
Let $R$ be a goal rewrite system for abduction.
The {\em computed rule for a literal $p$} is defined as:
If $p \rightarrow_R F$, the computed rule for $p$ 
is the rewrite 
rule $p \rightarrow F$; 
if 
\begin{eqnarray*}
&& p \rightarrow_R [l_{11}(C_{11})\land\cdots\land l_{1k_{1}}(C_{1k_{1}})] \vee \ldots \vee\\
&&\hspace*{2em}  [l_{m1}(C_{m1})\land\cdots\land l_{mk_{m}}(C_{mk_{m}})]
\end{eqnarray*}
such that each $l_{ij}$ is either $T$ or 
an abducible literal, and
$C_{i1}\cup\cdots\cup C_{ik_i}$ is consistent for each $i$,
then the computed rule for $p$ is the rewrite 
rule 
\begin{eqnarray}
&& p \rightarrow [l_{11}(C_{11})\land\cdots\land l_{1k_{1}}(C_{1k_{1}})] \vee \ldots \vee \nonumber \\
&&\hspace*{2em}  [l_{m1}(C_{m1})\land\cdots\land l_{mk_{m}}(C_{mk_{m}})]
\label{computedrule}
\end{eqnarray}
\end{definition}
\vspace{.1in}
\noindent
\underline{\bf Recycling Rule:}  \\
Let $g_1 \prec^+ g_n\prec p$ be a rewrite chain where $p$ 
is a non-loop literal.
Let $G = \{g_1,...,g_n,p\}$, and (\ref{computedrule})
be the computed rule for 
$p$. 
Then, the {\em recycling rule} for $p$
is defined as:
\begin{itemize}
\item [RC'.]
\begin{eqnarray*}
&& p \rightarrow [l_{11}(C_{11}\cup G)\land\cdots\land l_{1k_{1}}(C_{1k_{1}}\cup G)] \vee \ldots \vee  \\
&&\hspace*{2em}  [l_{m1}(C_{m1}\cup G)\land\cdots\land l_{mk_{m}}(C_{mk_{m}}\cup G)]
\end{eqnarray*}
\end{itemize}

Now given an abductive rewrite system 
$R^0=\langle {\cal Q}_L, {\cal R}_P, A, \rightarrow \rangle$. Recursively,
let $R^n$ be the rewrite system obtained from $R^{n-1}$ by replacing
the rewrite rules for {\em some} of the literals by their 
corresponding recycling rules. Notice here that $R^n$ is obtained
from $R^{n-1}$ nondeterministically by choosing some of the
literals whose answers have been computed in $R^{n-1}$, and replace
their rewrite rules by these computed answers.
Both Theorems~\ref{main2} and \ref{main3} can be extended to $R^i$
for any $i\geq 0$.

\begin{theorem}
\label{main-theorem2}
Let $P$ be a finite program, $A$ a set of abducibles, and
$R^0=\langle {\cal Q}_L, {\cal R}_P, A, \rightarrow \rangle$
the goal rewrite system with respect to $P$ and $A$. For any
$i>0$, let $R^i$ be defined as above.

\vspace{.1in}
\noindent
{\sf Soundness:} For any literal $g$ and any rewrite sequence
\[
g \rightarrow^*_{R^i} G \vee [l_1(C_1)\land\cdots\land l_k(C_k)] \vee G',\]
where each $l_i$ is either an abducible literal or $T$,
if $C_1\cup\cdots\cup C_k$ is consistent, then
there exists a partial stable model
$M$ of $P\cup \{l_1,...,l_k\}^+$
such that $g \in \bigcup_{1\leq j\leq k} C_i \subseteq M$.

\vspace{.1in}
\noindent
{\sf Completeness:} For any set of atoms $S\subseteq A$, and any
literal $g$ in 
a partial stable model $M$ of $P\cup S$,
there exists a rewrite sequence
\[
g \rightarrow^*_{R^i} G\vee [l_1(C_1)\land\cdots\land l_k(C_k)] \vee G',\]
such that
$g \in \bigcup_{1\leq j\leq k} C_j \subseteq M$.
\end{theorem}
\begin{INproof}
Similar to the proof of Theorem~\ref{main-theorem}.
\end{INproof}

\begin{theorem}  
\label{main4}
Let $P$ be a finite program, and
$R^0=\langle {\cal Q}_L, {\cal R}_P, A, \rightarrow \rangle$
a goal rewrite system. Let $R^i$ be as defined above, $i>0$.
Suppose $q$ is a proposition and
\begin{eqnarray*}
&& q \rightarrow^*_{R^i} [l_{11}(C_{11})\land\cdots\land l_{1k_{1}}(C_{1k_{1}})] \vee \ldots \vee\\
&&\hspace*{2em}  [l_{m1}(C_{m1})\land\cdots\land l_{mk_{m}}(C_{mk_{m}})]
\end{eqnarray*}
is a rewrite sequence such that each $l_{ij}$ is either $T$ or 
an abducible literal, and
$C_{i1}\cup\cdots\cup C_{ik_i}$ is consistent for each $i$.
If $P$ has no odd loops then
\[ \{
\{ l_{11},\cdots,l_{1k_{1}}\}, \cdots,
\{ l_{m1},\cdots,l_{mk_{m}}\} \}
\]
is a cover of $q$. In general, for arbitrary $P$ we have
\[ 
\bigvee_{\alpha\in \cal S}\alpha \supset
[l_{11}\land\cdots\land l_{1k_{1}}]\lor \cdots\lor
[l_{m1}\land\cdots\land l_{mk_{m}}]
\]
where $\cal S$ is any cover of $q$. 
\end{theorem}
\begin{INproof}
Just like the proof of Theorem~\ref{main3} in \cite{linyou02}.
\end{INproof}

\section{A Recycling Strategy}
\label{strategy}

We have shown that in theory one can reuse the previously
computed answers in our rewrite systems for abduction. 
To put the
theory into practice, we need some effective strategies on how
to recycle these computations. 

First, we shall further motivate the need for good recycling strategies.
Since a set of previously computed answers may not be actually used in
answering a new goal, recycling in general does not change 
the complexity of deciding 
whether a goal is true in a partial stable model of a program.
However, recycling sometimes can reduce the computation of a hard goal
to a trivial one simply due to the fact that the real hard part of the current 
goal has already been computed and can be used
directly in proving the current goal.
%It is easy to see that a proof is guaranteed to be shortened whenever a 
%previously computed answer is used.

However, the benefit of recycling does not come free:  
recycling incurs overhead, sometimes substantial overhead.
In the worse case, since there can be an exponential 
number of (partial) stable models for a program, there can be an exponential 
number of explanations for an observation. 
Saving all of them can be expensive.
Furthermore, one needs to check against the list of 
computed literals during computation. So, it is easy to construct 
an example where computation becomes less efficient due to 
overhead. %and no benefit of recycling.
Thus, the effectiveness of 
recycling depends on a good strategy that previously computed results are 
likely to be used. In this section we present such a strategy.

If we want to compute the abduction of all goals in a set, without the
framework of recycling introduced here, the only way is to compute them
one by one independently. With the idea of recycling, we can try to 
recycle previously computed answers. The question is then which goals
to compute first. This question arises even if we just want to
compute the abduction of a single goal:
instead of computing it using the original program, it may sometimes
be better if we first
compute the abduction of some other goals and recycle the results.

Assuming that goals are literals, a
simple strategy for deciding the order of goals to be computed
is to find out the dependency relations among the goals.

\begin{definition}
A literal $l$ is said to be depending on a literal $l'$ if the atom in
$l$ depends on the atom in $l'$. 
An atom $p$ is said to be depending on an atom
$q$ if either $q$ is in
the body of a rule whose head is $p$ or inductively, there is another
atom $r$ such that $p$ depends on $r$, and $q$ is in the body
of a rule whose head is $r$.
\end{definition}

Suppose $l'$ depends on $l$, but $l$ does not depend
on $l'$, written $l<l'$ below. It is easy to see that
$l$ will never be sub-goaled to $l'$ during rewriting, but
$l'$ could be sub-goaled to $l$. Thus if we need to compute the abduction
of both $l$ and $l'$, we should do it for $l$ first. 

This strategy, and as we have mentioned above 
in general rewrite with computed rules, is not
guaranteed to be more efficient computationally:
\begin{itemize}
\item $l<l'$ does not imply that a proof of $l'$ must go through $l$. For
instance, it could be that all rewrite chains for $l'$ terminate with
failure before $l$ is reached.
\item Even if we have a computed rule for $l$, using it in the proof of
$l'$ does not always result in computational gains.
For instance, suppose the computed rule for $l$ is
\[
l \rightarrow_R T(C_1)\lor\cdots\lor T(C_n),
\]
and a rewrite chain for $l'$ is $l\rightarrow^* T(C)\land l$. If $C$ is
inconsistent with all $C_i$'s, then this rewrite chain will terminate with $F$
after trying out all $n$ different proofs of $l$ using the computed rule
for $l$. However, if we do not use the computed rule for $l$, it may well be
that after only one step of expanding $l$, a contradiction is detected.
\end{itemize}
However, there is one case of recycling that
is almost trivial to implement, yet
its effectiveness is independent
of any strategy of rewriting. This is the case of recycling  
only failed proofs. That is, if the computed rule for $l$ is 
$l\rightarrow_R F$, then using this computed rule for $l$ in the proof
of another goal is always as good as the one without. More precisely,
if a terminating rewrite chain of $q$ goes through $l$ but does not
use the computed rule for $l$, then there is another terminating 
rewrite chain of $q$ that uses the computed rule for $l$, and has the same
or fewer number of steps than the original rewrite chain.
It is impossible to quantify the computational gains in terms of 
worst-case complexity analysis. In practice, we expect it to be very
effective as our following experiment shows.


\section{Experiments}
\label{experiments}

We have implemented a depth-first search rewrite procedure with 
branch and bound. The procedure can be used to 
compute explanations using a nonground program,
under the condition that  
in each rule
a variable that appears in the body must also appear in the head. 
When this condition 
is not satisfied, one only needs to instantiate those variables that only appear 
in the body of a rule.

To check the
effectiveness of the idea of recycling, 
we consider an
application of abduction in logic programming, the problem
of computing successor
state axioms from a causal action theory \cite{lin-95,LinWang99,Lin:jair03}.

Consider a logistics domain in which we have a truck and a package. We know
that the truck and the package can each be at only one location at any given
time, and that if the package is in the truck, then when the truck moves
to a new location, so is the package. Suppose that we have the following 
propositions:
\begin{itemize}
\item
$\ta(x)$ \--- the truck is at location $x$ initially;
\item
$\pa(x)$ \--- the package is at location $x$ initially;
\item
$\inm$ \--- the package is in the truck initially;
\item
$\ta(x,y,z)$ \--- the truck is at location $x$ after the action of moving
it from $y$ to $z$ is performed;\footnote{Suppose $move(y,z)$ stands for the
action of driving the truck from locations $y$ to $z$, and the current
situation is $s$, then in situation calculus, this proposition can be
written as $holds(ta(x),do(move(y,z),s))$. Our representation is sufficient
here since we only consider one type of actions, and two situations: the
initial one, and the one after the execution of the action.}
\item
$\pa(x,y,z)$ \--- the package is at location $x$ after the action of moving
the truck from $y$ to $z$ is performed; and
\item
$\inm(y,z)$ \--- the package is in the truck after the action of moving
the truck from $y$ to $z$ is performed.
\end{itemize}
We then have the following logic program:\footnote{See \cite{LinWang99} for
how logic programs of this kind can be used to encode a class of causal action theories.}
\begin{eqnarray}
&& \ta(X,X1,X). \label{ta1}\\
&&
\pa(X,X1,X2) \leftarrow \ta(X,X1,X2), \inm(X1,X2).\nonumber 
\\
&& \ta(X,X1,X2) \leftarrow X \neq X2,
    \ta(X), \Not \taol(X,X1,X2).\nonumber \\
&&
\taol(X,X1,X2) \leftarrow Y \neq X, \ta(Y,X1,X2).\nonumber \\
&& \pa(X,X1,X2) \leftarrow 
    \pa(X), \Not \paol(X,X1,X2).\nonumber \\
&& \paol(X,X1,X2) \leftarrow  Y \neq X, \pa(Y,X1,X2).\nonumber \\
&& \inm(X,Y) \leftarrow \inm.\label{in}
\end{eqnarray}
The first rule is the effect axiom. The second rule is a causal rule which
says that if a package is in the truck, then the package should be where
the truck is. The rest are frame axioms. For instance, the third one
is the frame axiom
about $\ta$, with the help of a new predicate $\taol$: if the truck is
initially at $X$, and if one cannot prove that it will be elsewhere after
the action is performed, then it should still be at $X$.

As one can see, the above program, when
fully instantiated over any given finite set $D$ of locations, 
has no odd loops. So our rewrite system will generate a cover
for any query. Note that in the program we have omitted 
domain predicate $loc(X)$ for each variable $X$ in the body
of a rule (all the variables in the program refer to 
locations). Thus, the program is domain restricted, and we
only need to instantiate the variable $Y$ in the fourth
and sixth rules over the domain of locations.

Now let the set $A$ of abducibles be the following set:
\[
\{ \inm\} \cup \{ \pa(x), \ta(x)\D x\in D\}.
\]
Our job here is then to compute the abduction of successor state
propositions
$$\{ \ta(x,y,z), \pa(x,y,z), \inm(y,z)\}$$
 in terms of these abducibles, which
are initial state propositions.
For instance, given query $\pa(3,2,3)$, our system would compute its
abduction as  $\pa(3)\lor\inm$, meaning that for 
it to be true, either
the package was initially at $3$ or it was inside the truck.

According to the definition in the last section,
literals that contain
$\pa(X,Y,Z)$ depend on those that contain
$\inm(X,Y)$ and  $\ta(X,Y,Z)$.
But literals that contain
$\inm(X,Y)$ and those that contain $\ta(X,Y,Z)$ do not depend on 
each other.
So we should compute first the abduction of $\inm(X,Y)$ and $\ta(X,Y,Z)$.
Now $\inm(X,Y)$ is solved by rule
(\ref{in}), $\ta(X,Y,X)$ by rule (\ref{ta1}), and as it turned out,
when $X\neq Z$, $\ta(X,Y,Z)$ is always false, and its computation is 
relatively easy.
 For instance, in our experiments
for the domain with 9 locations, query $\ta(7,1,6)$ took only 2.6 seconds.
In comparison, query $\pa(7,1,7)$ took more than 7000 seconds without
recycling.

Table~\ref{data} contains run time data for some representative 
queries.\footnote{Our implementation was written in Sicstus Prolog, and
the experiments were done on a PIII 1GHz notebook with 512 MB memory. 
%For generating explanations for regular rewriting system, 
This implementation
is a significant improvement over the one in \cite{linyou02}. For instance, 
for a domain with 7 locations query $\pa(3,2,3)$ took more than
20 minutes for
the implementation reported in \cite{linyou02}, but required less than
1 second under our implementation running on a comparable machine.}
For comparison purpose, 
each query is given two entries:
the one under ``NR'' refers to regular rewriting system 
without using recycling,
and the one under ``WR'' refers to rewriting system using computed
rules about $\ta(X,Y,Z)$. As one can see, especially for hard queries like
$\pa(7,1,7)$, recycling in this case significantly speeds up the 
computation.
\begin{table}
\begin{tabular}{|c|c|c||c|c|}
\hline Query & \multicolumn{2}{|c||}{9 locations} &
\multicolumn{2}{|c|}{10 locations} \\
\cline{2-5} & NR & WR & NR & WR\\
\hline
pa(1,2,3)  &     0.71 &   0.41 &     1.50 &  0.89 \\
-pa(1,2,3) &    75.89 & 2.28 &  342.96 & 5.65    \\
%pa(2,2,3)  &    0.71 & 0.40 &    1.51 & 0.90       \\
%-pa(2,2,3) &    76.12 & 2.29 &  343.68 & 5.67        \\
pa(3,2,3)  &    137.05 &  0.89 &  630.69 & 1.98         \\
-pa(3,2,3) &      2.97 & 1.98 &   7.64 &  5.03           \\
pa(1,5,7) &  122.87 &0.75 & 278.07 &1.31    \\
-pa(1,5,7) & 727.6 & 7.07 &2534.09 & 19.08      \\
pa(7,5,1) &  108.66 &  17.82 & 188.50 & 30.72        \\
-pa(7,5,1) &  74.43 &2.26 & 340.51 &5.64          \\
%pa(6,3,6) &    737.54 &3.91 &2285.40 &6.29          \\
%-pa(6,3,6) &   2.96 &2.02 &   7.69 &5.04       \\
pa(7,1,7) & 7619.72 &  20.78 & 29140.69 & 35.65       \\
-pa(7,1,7) &  2.98 &2.01 &   7.71 &5.05       \\
\hline
\end{tabular}
\caption{Recycling in logistics domain. Legends: NR - no recycling; WR - 
recycling $\ta(X,Y,Z)$ goals. All times are in CPU seconds.}
\label{data}
\end{table}

\section{Extensions and related work}

\subsection{Some Extensions}

So far we have assumed that the given logic program is propositional,
and does not contain constraints. We discussed in \cite{linyou02} some
possible extensions. Firstly,
our rewrite systems work on a nonground program,
under the condition that  
in each rule
a variable that appears in the body must also appear in the head. 
Under this condition, an observation (a ground goal) 
is always rewritten to another ground goal, so that a rewriting mechanism
designed for ground programs works just as well.
When the condition 
is not satisfied, one only needs to instantiate those variables that only appear 
in the body of a rule.
For example, domain restricted programs \cite{niemela-amai-long}
can be instantiated only on domain predicates for variables that do not appear in the head. This is a significant departure from the approaches that are based on
ground computation where a function-free program is first instantiated to 
a ground program with which the intended 
models are then computed.

Constraints of the form
$$\bot \leftarrow a_1,...,a_i,\Not b_1,...,\Not b_n.$$
can be handled 
in our rewriting procedure just like in
other abductive procedures \cite{devecker92JLP,fungJLP,k-m-mJLP00}:
namely, a goal is proved along with all the constraints. 
This ensures that all of the constraints are satisfied when the goal is proved.

\begin{example}
Consider the following program and constraint:
\[
\begin{array}{ll}
a \leftarrow \Not b. ~~~ b \leftarrow \Not a. ~~~ c \leftarrow c.\\
\bot \leftarrow b, \Not c.\\ 
\end{array}
\]
In trying to prove $b$, for example, the goal formula including the constraint
is 
$b \wedge \neg (b \wedge \neg c)$, 
which reduces to 
$b \wedge (\neg b \vee c)$.
The following rewrite sequence shows that 
there is no partial stable model that contains $b$ while satisfying the 
given constraint.
$$
\begin{array}{ll}
b \wedge (\neg b \vee c)\\
\rightarrow (b \wedge \neg b) \vee (b \wedge c) \rightarrow ......\\
\rightarrow F \vee (b \wedge c)
\rightarrow b \wedge c
\rightarrow \neg a \wedge c
\rightarrow b \wedge c \\
\rightarrow T(\{b,\neg a\}) \wedge c
\rightarrow T(\{b,\neg a\}) \wedge c
\rightarrow T(\{b,\neg a\}) \wedge F
\rightarrow F
\end{array}
$$
\end{example}





However, computationally this is not a very effective approach when there
are many constraints. Since a rewrite chain in our system carries a
context with it, we could check the consistency of this context
with the given constraints. This can be done by adding
the following
simplification rule:
\[
T(C) \rightarrow F, \mbox{ if $C$ violates a constraint}
\]
Here we say that a context $C$ violates a constraint $\bot\leftarrow G$
if $G$ is a subset of $C$.

However, this approach may not be ``sound'', 
for the same reason that
our rewrite system is only sound under partial stable model semantics, but
not under the stable model semantics. Consider the following program:
\[
p.\ \ \ \bot\leftarrow p, q.\ \ \ \bot\leftarrow p, \Not q.
\]
There is a rewrite of $p$ to $T$
under the context $\{p\}$, which does not violate
any of the constraints according to our definition. However, $p$ should not
be ``proved'' as the context cannot be extended to one that satisfies both
of the constraints. But this is the same reason why our rewrite
system is not sound under the stable model semantics: a program may not
have a stable model (for instance with $a\leftarrow \Not a$ the only rule
whose head is $a$), but a goal may be written to $T$ (for instance for
a goal that does not mention $a$). So perhaps this strategy of dealing with
constraints matches well with our rewrite systems, which are sound and
complete under the partial stable model semantics.


\subsection{Related work}

We discussed in \cite{linyou02} how our rewrite systems for abduction
are related to other abductive systems, e.g. \cite{consoleJLP91,devecker92JLP,ek89-long,fungJLP,k-k-t-95,k-m-90,k-m-mJLP00,satoh-92-long}. 
One useful way of looking at an abductive logic programming system is
the underlying semantics the system is based on. For instance, The
rewrite-like systems in \cite{consoleJLP91,fungJLP,Hayashi98-long} are 
based on Clark's completion semantics, the systems in \cite{devecker92JLP,Kakas2001}
are for well-founded models, and the procedure in \cite{ek89-long} is
sound and complete under the finite-failure three-valued semantics
in which loops causing infinite failure
are modeled by the truth value {\em undefined} \cite{girJLP}.



Our rewrite systems were designed with the stable model semantics
in mind. As we see in section~\ref{abduction}, we 
defined basic notions of
abduction in logic programming, such as explanations, minimal
explanations, and covers of explanations in terms of the stable
model semantics. However, our rewrite systems are goal-directed,
thus check for local consistency only. For instance, unless 
the atom $a$ is ``related to'' to the query $q$, a rewrite
chain starting at $q$ would never reach $a$, thus would never
check the consistency implicitly given by the odd loop $a\leftarrow \Not a$.
Thus our rewrite systems are sound and complete only under the
partial stable model semantics.

According to \cite{20KR-ACM}, given
any normal or disjunctive program $P$, there is a polynomial time translation
from $P$ to $P'$ such that a query is true in an answer set of $P$
if and only if it is true in a partial stable model of $P'$
(see Corollaries 3.15-16 of \cite{20KR-ACM}). So, query answering under 
the answer set semantics can be carried out by
query answering under the semantics based on partial stable models. Thus,
our rewrite systems are applicable to the stable model semantics 
as well. 

One can also apply the technique of rewriting for the 
answer set semantics without carrying out a transformation, as we outlined 
following Theorem~\ref{main2}.

We note that recycling in our case differs from 
the reuse of hypotheses in the abductive procedures 
in \cite{ek89-long,k-m-90p,k-m-mJLP00}.
In the latter case, hypotheses are saved as individuals for the purpose 
of checking consistency while in our case, the computed answers are saved.
It is interesting to see that consistency check in our rewrite procedures
is already captured by the loop detection mechanism
as defined in Section~\ref{review}. The advantage of loop detection
is that not only the completeness is guaranteed but also the procedure 
is terminating for propositional programs. 

\section{Concluding remarks and future work}



We have considered the problem of how to reuse previously computed
 results
for answering other queries in the abductive rewriting system of 
Lin and You \cite{linyou02} for logic programs with negation, and showed
that this can indeed be done. We have also described a methodology of 
using the recycling system in practice by analyzing the dependency relationship
among propositions in a logic programs. We applied this methodology to
the problem of computing the effect of actions in a logistics domain, the
same one considered in \cite{linyou02}, and 
our experimental results showed that recycling in this domain can 
indeed result in good performance gain.


For future work we are looking for more domains to try our system on and
to implement a system that can
automatically analyze a program and decide how best to recycle previous
computations.


\begin{acks}
We would like to thank the reviewers of this paper
for their thoughtful comments.
Fangzhen Lin's work was supported in part
by 
the Research Grants Council of Hong Kong
under Competitive Earmarked Research Grant HKUST6205/02E.
\end{acks}

\bibliographystyle{acmtrans}            

\begin{thebibliography}{}

\bibitem[\protect\citeauthoryear{Console, Theseider, and Porasso}{Console
  et~al\mbox{.}}{1991}]{consoleJLP91}
{\sc Console, L.}, {\sc Theseider, D.}, {\sc and} {\sc Porasso, P.} 1991.
\newblock On the relationship between abduction and deduction.
\newblock {\em J. Logic Programming\/}~{\em 2(5)}, 661--690.

\bibitem[\protect\citeauthoryear{Denecker and Schreye}{Denecker and
  Schreye}{1998}]{devecker92JLP}
{\sc Denecker, M.} {\sc and} {\sc Schreye, D.~D.} 1998.
\newblock {SLDNFA}: an abductive procedure for normal abductive programs.
\newblock {\em J. Logic Programming\/}~{\em 34,\/}~2, 111--167.

\bibitem[\protect\citeauthoryear{Dershowitz and Jouannaud}{Dershowitz and
  Jouannaud}{1990}]{dershowitz90}
{\sc Dershowitz, N.} {\sc and} {\sc Jouannaud, P.} 1990.
\newblock Rewrite systems.
\newblock In {\em Handbook of Theoretical Computer Science, Vol B: Formal
  Methods and Semantics}. North-Holland, 243--320.

\bibitem[\protect\citeauthoryear{Dix}{Dix}{1991}]{dix-91}
{\sc Dix, J.} 1991.
\newblock Classifying semantics of logic programs.
\newblock In {\em Proc. First Workshop on Logic Programming and Nonmonotonic
  Reasoning}. MIT Press, 167--180.

\bibitem[\protect\citeauthoryear{Dung}{Dung}{1991}]{dun-91}
{\sc Dung, P.} 1991.
\newblock Negations as hypothesis: An abductive foundation for logic
  programming.
\newblock In {\em Proc. 8th International Conference on Logic Programming}. MIT
  press, 3--17.

\bibitem[\protect\citeauthoryear{Dung}{Dung}{1995}]{dun-95-1}
{\sc Dung, P.} 1995.
\newblock An argumentation theoretic foundation for logic programming.
\newblock {\em J. Logic Programming\/}~{\em 22}, 151--177.

\bibitem[\protect\citeauthoryear{Eshghi and Kowalski}{Eshghi and
  Kowalski}{1989}]{ek89-long}
{\sc Eshghi, K.} {\sc and} {\sc Kowalski, R.} 1989.
\newblock Abduction compared with negation by failure.
\newblock In {\em Proc. 6th International Conference on Logic Programming}. MIT
  Press, 234--254.

\bibitem[\protect\citeauthoryear{Fages}{Fages}{1994}]{fages94}
{\sc Fages, F.} 1994.
\newblock Consistency of {C}lark's completion and existence of stable models.
\newblock {\em Journal of Methods of Logic in Computer Science\/}~{\em 1},
  51--60.

\bibitem[\protect\citeauthoryear{Fung and Kowalski}{Fung and
  Kowalski}{1997}]{fungJLP}
{\sc Fung, T.} {\sc and} {\sc Kowalski, R.} 1997.
\newblock The iff proof procedure for abductive logic programming.
\newblock {\em J. Logic Programming\/}~{\em 33,\/}~2, 151--164.

\bibitem[\protect\citeauthoryear{Gelfond and Lifschitz}{Gelfond and
  Lifschitz}{1988}]{g-l-88-long}
{\sc Gelfond, M.} {\sc and} {\sc Lifschitz, V.} 1988.
\newblock The stable model semantics for logic programming.
\newblock In {\em Proc. 5th International Conference on Logic Programming}. MIT
  Press, 1070--1080.

\bibitem[\protect\citeauthoryear{Giordano, Martelli, and Sapino}{Giordano
  et~al\mbox{.}}{1996}]{girJLP}
{\sc Giordano, L.}, {\sc Martelli, A.}, {\sc and} {\sc Sapino, M.} 1996.
\newblock Extending negation as failure by abduction: A three-valued stable
  model semantics.
\newblock {\em J. Logic Programming\/}~{\em 26,\/}~1, 31--67.

\bibitem[\protect\citeauthoryear{Hayashi}{Hayashi}{1998}]{Hayashi98-long}
{\sc Hayashi, H.} 1998.
\newblock Knowledge assimilation and proof restoration through the addition of
  goals.
\newblock In {\em Proc. 8th International Conference on Artificial
  Intelligence: Methodology, Systems, and Applications}. LNCS 1480. 291--302.

\bibitem[\protect\citeauthoryear{Janhunen, Niemel{\"{a}}, Seipel, Simons, and
  You}{Janhunen et~al\mbox{.}}{2004}]{20KR-ACM}
{\sc Janhunen, T.}, {\sc Niemel{\"{a}}, I.}, {\sc Seipel, D.}, {\sc Simons,
  P.}, {\sc and} {\sc You, J.} 2004.
\newblock Unfolding partiality and disjunctions in stable model semantics.
\newblock In {\em ACM Transactions on Computational Logic}. To appear.

\bibitem[\protect\citeauthoryear{Kakas, Kowalski, and Toni}{Kakas
  et~al\mbox{.}}{1995}]{k-k-t-95}
{\sc Kakas, A.}, {\sc Kowalski, R.}, {\sc and} {\sc Toni, F.} 1995.
\newblock The role of abduction in logic programming.
\newblock In {\em Handbook of Logic in Artificial Intelligence and Logic
  Programming}. Oxford University.

\bibitem[\protect\citeauthoryear{Kakas and Mancarella}{Kakas and
  Mancarella}{1990a}]{k-m-90}
{\sc Kakas, A.} {\sc and} {\sc Mancarella, P.} 1990a.
\newblock Generalized stable models: a semantics for abduction.
\newblock In {\em Proc. 9th European Conference on Artificial Intelligence}.
  285--291.

\bibitem[\protect\citeauthoryear{Kakas and Mancarella}{Kakas and
  Mancarella}{1990b}]{k-m-90p}
{\sc Kakas, A.} {\sc and} {\sc Mancarella, P.} 1990b.
\newblock On the relation between truth maintenance and abduction.
\newblock In {\em Proc. PRICAI'90}. 438--443.

\bibitem[\protect\citeauthoryear{Kakas, Michael, and Mourlas}{Kakas
  et~al\mbox{.}}{2000}]{k-m-mJLP00}
{\sc Kakas, A.}, {\sc Michael, A.}, {\sc and} {\sc Mourlas, C.} 2000.
\newblock {ACLP}: abductive constraint logic programming.
\newblock {\em J. Logic Programming\/}~{\em 44,\/}~1-3, 129--178.

\bibitem[\protect\citeauthoryear{Kakas, {van Nuffelen}, and Denecker}{Kakas
  et~al\mbox{.}}{2001}]{Kakas2001}
{\sc Kakas, A.}, {\sc {van Nuffelen}, B.}, {\sc and} {\sc Denecker, M.} 2001.
\newblock {A-system}: problem solving through abduction.
\newblock In {\em Proc. IJCAI'01}. 591--596.

\bibitem[\protect\citeauthoryear{Lin}{Lin}{1995}]{lin-95}
{\sc Lin, F.} 1995.
\newblock Embracing causality in specifying the indirect effects of actions.
\newblock In {\em Proc. IJCAI'95}. Morgan Kaufmann Publishers, 1985--1993.

\bibitem[\protect\citeauthoryear{Lin}{Lin}{2003}]{Lin:jair03}
{\sc Lin, F.} 2003.
\newblock Compiling causal theories to successor state axioms and {STRIPS}-like
  systems.
\newblock {\em Journal of Artificial Intelligence Research\/}~{\em 19},
  279--314.

\bibitem[\protect\citeauthoryear{Lin and Wang}{Lin and Wang}{1999}]{LinWang99}
{\sc Lin, F.} {\sc and} {\sc Wang, K.} 1999.
\newblock From causal theories to logic programs (sometimes).
\newblock In {\em Proc. 5th International Conference on Logic Programming and
  Nonmonotonic Reasoning, LNCS 1730}. 117--131.

\bibitem[\protect\citeauthoryear{Lin and You}{Lin and You}{2001}]{linyou02}
{\sc Lin, F.} {\sc and} {\sc You, J.} 2001.
\newblock Abduction in logic programming: a new definition and an abductive
  procedure based on rewriting.
\newblock In {\em Proc. IJCAI'01}. 655--661.
\newblock The full paper appears in {\em Artificial Intelligence} 140(1/2):
  175-205 (2002).

\bibitem[\protect\citeauthoryear{Lin and Zhao}{Lin and
  Zhao}{2004}]{LinZhao:assat}
{\sc Lin, F.} {\sc and} {\sc Zhao, Y.} 2004.
\newblock {ASSAT: C}omputing answer sets of a logic program by {SAT} solvers.
\newblock {\em Artificial Intelligence\/}~{\em 157(1-2)}, 115--137.

\bibitem[\protect\citeauthoryear{Niemel{\"{a}}}{Niemel{\"{a}}}{1999}]{niemela-%
amai-long}
{\sc Niemel{\"{a}}, I.} 1999.
\newblock Logic programs with stable model semantics as a constraint
  programming paradigm.
\newblock {\em Annual of Mathematics and Artificial Intelligence\/}~{\em
  25,\/}~3-4, 241--273.

\bibitem[\protect\citeauthoryear{Przymusinski}{Przymusinski}{1990}]{prz-90b}
{\sc Przymusinski, T.} 1990.
\newblock Extended stable semantics for normal and disjunctive logic programs.
\newblock In {\em Proc. 7th International Conference on Logic Programming}. MIT
  Press, 459--477.

\bibitem[\protect\citeauthoryear{Sato}{Sato}{1990}]{sato90}
{\sc Sato, T.} 1990.
\newblock Completed logic programs and their consistency.
\newblock {\em J. Logic Programming\/}~{\em 9,\/}~1, 33--44.

\bibitem[\protect\citeauthoryear{Satoh and Iwayama}{Satoh and
  Iwayama}{1991}]{s-i-91}
{\sc Satoh, K.} {\sc and} {\sc Iwayama, N.} 1991.
\newblock Computing abduction using the {TMS}.
\newblock In {\em Proc. 8th International Conference on Logic Programming}. MIT
  Press, 505--518.

\bibitem[\protect\citeauthoryear{Satoh and Iwayama}{Satoh and
  Iwayama}{1992}]{satoh-92-long}
{\sc Satoh, K.} {\sc and} {\sc Iwayama, R.} 1992.
\newblock A query evaluation method for abductive logic programming.
\newblock In {\em Proc. Joint International Conference and Symposium on Logic
  Programming}. MIT Press, 671--685.

\bibitem[\protect\citeauthoryear{Simons}{Simons}{2000}]{smodels}
{\sc Simons, P.} 2000.
\newblock Smodels: a system for computing the stable models of logic programs,
  version 2.26.
\newblock At {\tt
  http://{\linebreak[3]}www.tcs.{\linebreak[3]}hut.fi/{\linebreak[3]}Software/%
{\linebreak[3]}smodels/}.

\bibitem[\protect\citeauthoryear{You and Yuan}{You and Yuan}{1995}]{y-y-95}
{\sc You, J.} {\sc and} {\sc Yuan, L.} 1995.
\newblock On the equivalence of semantics for normal logic programs.
\newblock {\em J. Logic Programming\/}~{\em 22}, 212--221.

\end{thebibliography}

\begin{received}
Received February 2004;
revised November 2004;
accepted April 2005
\end{received}

\end{document}



