Dear Reviewer:

Thank you for reviewing our paper, and for your comments about it. We 
list below our responses in the context of your report. To
make it easier for you to identify our responses, we start each of them
with ">>", and end it with "<<"

========
Report A
========

Recommendation: The paper can eventually be accepted for TOCL.
Another refereeing round is needed.

Overall comments:
This paper proposes a method of recycling previous proofs for parts of
a new proof in terms of partial stable model semantics. The method
stores a context of a previous derived results and reuses when there
is no contradiction between the current context for a new proof.

As far as I know, no one has ever consider recycling a proof in
nonmonotonic reasoning framework and therefore this is very
interesting paper. However, it seems to me that the
authors do not properly show a range of its applicability.
For example, 
(a) Would the method reduce computational complexity?

>> No. See section 6, page 24. <<

(b) If not, are there any class whose computational complexity
is reduced by proof recycling.

>> Yes, See the last paragraph of Section 6, page 25. <<


(c) Can this method handle function symbols or not? It is
rather dubious since all the examples are function-free examle.

>> We have made it clear that we are dealing with propositional
case only. The extension to rules with variables is discussed in
section 3.4, page 8. <<

(d) Can this method handle integrity constraints?
This question is important since integrity constraints play
an important role in abduction as in Eshghi-Kowalski procedure.

>> Yes. See section 3.4, page 9. <<

Therefore, I would like to know applicability of their method more
clearly. See the details below.
================================================================
Detailed Comments:
1. Firstly, I would like to comment on the previous work of
a rewriting system on which the current paper is based.

1-1. The title:
The title is misleading. I feel that the main point of
this paper is to recycle a proof in partial stable model
semantics. Abduction is only mentioned in the very small
part and does not seem so essential to me.

>> We have greatly expanded the section on abduction, and made it clear
that abduction is the application that we had in mind. See section 5,
page 18.
<<

1-2. Application of abduction in partial stable models:
Abduction in partial stable model semantics is not widely used, but
one in ordinary stable model semantics is used. For example, in stable
model semantics, people uses odd loop to express integrity constraint,
but we cannot do the same thing in partial stable model semantics
since an odd loop gives undefined value of related literals with the
odd loop. It is better that the authors show that there are some
concrete application of abduction in partial stable models.

>> We added some discussions about why we used partial
stable model semantics, and how our rewrite systems can be extended/adapted
for stable models semantics. See section 3.5, pages 10-11.
<<

1-3. Integrity constraints:
I believe that integrity constraints is very important
in abduction since they prevent unwanted conclusions.However,
this paper only considers an abduction without integrity
constraints.
For example, consider the following example:
\bot <- p. (\bot means falsity)
p <- q.
q <- not r.
r <- not q.

The above three rules would be translated to the following:
p<->q.
r<->not q.
q<->not r.

Then, for a derivation of q, q->not r->q->T(q,not r).

However, according to integrity constraint, it should be
failed. I do not see how to use a rewriting method in order
to detect this failure. The authors should mention the
treatment of the integrity constraints in more depth.

>> addressed above.<<

1-4. Computing minimal abducibles:
In similar work, done by Fung and Kowalski[1], they give a method of
computing minimal abducibles in terms of set-inclusion. Does the
procedure in the paper guarantee this?  In some applications such as
diagnosis, minimal fault hypotheses is preferable and so, if the
rewriting technique guarantees this, it would be interesting.

[1] Fung and Kowalski, The iff proof procedure for abductive logic
programming, JLP, vol. 33 151-164 (1997).

>> "Minimality" is a tricky issue in abductive logic programming.
One of the main conceptual contributions of our earlier paper [22]
was a new notion of explanations and minimal explanations, and
shifted the focus from computing so called minimal explanations
to what we called a "cover" of a query. Some of these  have been
duplicated in section 5.1, pages 18-20, of the paper. So the short answer
to this question is that, no, there is no guarantee that our procedure
would return a minimal explanation, and for a good reason.
<<

1-5. Related Work:
From my understanding, the authors' method is a kind of "traversing a
frontier" version of a search tree in Eshghi-Kowalski proof
procedure. In this respect, this paper is closely related with
Hayashi's work[2].  He provided an extended proof procedure which does
not separate a consistency phase and an abductive phase in E-K
procedure and keeps "frontier" of reduced goals. His aim is not for
recycling a proof, but for restoring a proof when additional
information is obtained during reasoning. From this viewpoint, the
authors' work might be applicable to the problem which he tried to
solve.

[2] Hisashi Hayashi: Knowledge Assimilation and Proof Restoration
Through the Addition of Goals. AIMSA 1998: 291-302

>> See our deicussion about related work in section 3.5. <<

1-6. Treatment of variable and function symbols.
From the definition of literal rewriting, there is no treatment of
variables, but in the example of experiments, there are variables in
the program. To me, if the simplification rules can handle variables,
the authors should clearly mentioned that in the definition of literal
rewriting. Also, I would like to know how to treat function symbols.

>> addressed above. <<
===================================================================
2. Now, I would like to comment on recycling part.
2-1. Computational complexity:
I do not believe that recycling reduces computational complexity of
question-answering in partial stable model semantics.  If the
reduction cannot be made, the authors should clearly state so. It
would be better if the author could give some classes where the
computational complexity is reduced by using proof recycling.

>> addressed above. <<

2-2 Is it always efficient?
The authors mentioned that recycling is not always efficient.  This is
an important result, but it is much better if the author gives some
classes where every proof is always shortened if we recycle a proof.

>> addressed above. <<

2-3 In stable model semantics, is recycling technique
efficient compared with answer set programming?
If there is no odd loop in a program, the partial stable
model semantics coincides with the stable model semantics.
So, in this class, this method can be compared with answer set
programming. I would like to know whether proof-recycling
technique always beats answer set programming systems such
as DLV or not.

>> We focus on comuting abduction here, instead of generating
stable models as in ASP. Also our recycling is about reusing
previous proofs. It would be interesting to compare query answering
using the rewrite procedures discussed here and that using a stable
model generator such as DLV, but we have not done any such 
experiments.
<<