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 B
========

- Recommendation: The paper can be accepted for TOCL after minor
revisions. No further refereeing round is needed.

I could have a quick look at the revised version.

This paper is a good effort to study in a formal way
the issue of loop checking and re-use of hypotheses
in computing abduction usually left at the level of
implementation for most other approaches of computing
abduction. Technically, the paper is sound and thorough
modulo some minor issues of clarity of presentation
(see below). The results are relatively straightforward
but non-trivial and it is useful to have them.

As one would expect its results are
only relevant for essentially propositional
theories (although the authors try to convince us
otherwise). It is not clear how these results
can be extended and used in more general forms
of computation of abduction such as in the
frameworks of ACLP, SLDNFA and IFF. Nevertheless,
the work has good value and should be published,
after the minor weakness of proper placement
and comparison with other related work is
corrected (see below).

A minor weakness of the paper that should be
corrected before publication is the fact that
the paper does not discuss related work for
the computation of abduction. 

>> There were extensive discussions about related work in our earlier 
work [22], and we have repeated some of them in section 3.5, page 10.
<<

On the one hand,
reference to the more recent work in abduction
as found in the following papers should be made:

@ARTICLE{,
  author =       {M. Denecker and D. De Schreye},
  title =        {{SLDNFA}: an abductive procedure for abductive logic 
programs},
  journal =      {Journal of Logic Programming},
  year =         {1998},
  volume =       {34},
  number =       {2},
  pages =        {111-167},
  publisher =    elsevier,
}

@inproceedings{,
    author = {A. C. Kakas and M. Denecker},
    title =        {Abduction in Logic Programming},
    editor =       {A. C. Kakas and F. Sadri},
  booktitle =    {Computational Logic: Logic Programming and Beyond. 
Part I},
  publisher =    SV,
  series =       LNAI,
  number =       {2407},
  year =         {2002},
  pages =        {402--436},
}

@INPROCEEDINGS{,
  AUTHOR =       "A. C. Kakas and B. {van Nuffelen} and M. Denecker",
  TITLE =        "{A-System}: Problem Solving through Abduction",
  BOOKTITLE =    IJCAI01,
  YEAR =         "2001",
  editor =       "B. Nebel",
  pages =        "591-596",
  address =      "Seattle, Washington, USA",
  publisher =    MKP,
}

@ARTICLE{,
  author =       {T. H. Fung and R. A. Kowalski},
  title =        {The {IFF} proof procedure for abductive logic 
programming},
  journal =      {Journal of Logic Programming},
  publisher =    elsevier,
  volume =       {33},
  number =       {2},
  year =         {1997},
  pages =        {151--165},
}

In particular,  SLDNFA, IFF and the Asystem all use
a computational model formalized in terms of
a set of rewrite rules. The operate on a
more general class of theories considered
in the paper.

On the other hand, some short
discussion of comparison with the way the
class of abductive proof procedures in
the paper's references [6,10,11] use
recycling of hypotheses is required.

These procedures include an important element
of reuse of abducible hypotheses during the
computation. Briefly, abducible literals
if required again during the computation
are not checked again for consistency
and when an abducible literal
and its complement are required in a branch
of the computation this branch is failed.
Hence these procedures have a similar
approach to reuse of computation but restricted
to abducible goals. On the other hand,
these works work more general theories and
more general forms of non-ground abduction.
For example, they can have integrity constraints and in fact
extract, during the computation information, form
these further abducible hypotheses that
can be reused in the subsequent computation
in the ways explained above.

>> We noted the differences between recycling in our
case, and the reuse of hypotheses in the work that
you cited in the 2nd paragraph of section 8, page 29.
<<

Regarding the empirical results of experimentation
presented in the paper one could argue that
the example used has been formulated appropriately
for the loop checking and reuse to have maximum effect.
The formalization is not canonical
that would easily extend to more complex forms
of the logistics problem with many packages
and trucks, other forms of transportation etc.
Hence the experimentation carried out is limited
and not very convincing. Also there is no independent
comparison with ASP systems such as SMODELS and DLV
or with other top-down abduction systems
such as the Asystem. Anything that you could
add along these lines would be a plus. But I do not
consider it necessary for publication except
that some short of statement of the limitations
of the experimentation should be given.

>> We have explained this example in much greater details.
As shown in [20], many planning domains can be axiomatized
in causal theories, which in turn can be represented as
logic programs of the form in the example [21].
<<

The clarity of presentation of some
of the technical aspects of the work can be
improved. I would recommend the following:

a) Give an explicit definition of Normal Form
of a goal and termination of rewriting. Without this
the reader finds it difficult to understand the
results in section 3.3 and thereafter.

>> Normal form: third line, page 8. Termination: Definition 3.4, page 7.
<<

b) Illustrate the confluent property with an example
after its definition 3.5.

>> Example 3.6, page 8 <<

c) Give the formal details of derivation trees and
what it means for a branch to succeed.

>> page 12 (i.e. ends with ...) <<

d) In section 5, the extension to abduction
is given too fast in the first paragraph for
some notation to be incomplete, e.g. what is
C in l(C) when l is abducible?
Present this extension more formally with
proper definitions.

>> Section 5 is greatly expanded. <<

Minor corrections are:

1) classic logic -> classical logic

2) endless -> infinite

3) page 11: The 2nd sentence of the 1st paragraph
"If a computed rule ...for p." is not clear.

4) Page 17: explain better the meaning of ta(x,y,z),
pa(x,y,z) and describe briefly what the program
rules say.

>> Done. See page 27. <<