%%%% CP's comment:
%%%% This is a trial to make the evaluation process of scientific
%%%% papers more bidirectional. 
%%%% If you think that this is against some etiquette, inappropriate,
%%%% or against good manners, please let me know and I will stop it!!!

An approach to the integration of induction 
-- in the form of implicit induction alias 'descente infinie' alias 
least number/element principle -- into analytic (free variable) tableaux
is presented.

Given the fact that very few is known about inductive reasoning in
tableau format this work is certainly timely and relevant.
Although the material is presented in a technically careful and
accurate form I found the paper not easy to read. This is certainly
in part because of my lack of knowledge in this area, but probably
also due to a slightly indiosyncratric terminology and style.
I think that the work would profit from a more thorough discussion
of its relation to other work in inductive theorem proving.
I also find it hard to judge the signifcance of the main results,
because no consequences are drawn that would allow to compare
the achievements of the author with that of other frameworks of
inductive theorem proving. However, the offered results seem to
both, correct and relevant to further investigations.

%%%% CP's comment:
%%%% The criticism is justified. I will try to be better in a journal
%%%% version with less space restrictions.

A minor item: After stating (on p.5) the relevant induction principle
the author writes: "Now by the Principle of Dependent Choice (cf. Rubin
& Rubin (1985)) ...".  I find this reference quite inappropriate: Of course,
one needs some form of the axiom of choice to prove the existence of minimal
elements _in general_, however in the context of inductive reasoning
the used ordering is always _concretely given_ and consequently the
fact that "a class without minimal elements contains a chain without a
least element" is always obvious in any particular scenario
of theorem proving.

%%%% CP's comment:
%%%% The problem is that there may be several counterexamples and the
%%%% induction order be partial. So you have to pick and pick and pick
%%%% smaller counterexamples from unstructured non-empty sets.

I also do not agree with the authors opinion (voiced at the beginning of
the introduction) that "analytic calculi can mirror the human proof search 
process better...". I am rather convinced that the significance of Gentzen's
analysis (among others) is based on the fact that, quite to the contrary, 
"human proof search" (as opposed to efficiently mechanizable proof search)
relies on cuts (i.e. modus ponens, lemmatization etc.).

%%%% CP's comment:
%%%% This was a misunderstanding. I have tried to be more precise in the
%%%% final version.

In spite of the mentioned criticsm, my general impression is a positive one.
I think that a presentation and discussion of this work is
valuable for the Tableau community and therefore recommend acceptance.