The author presents versions of the (classical) 
sequent and tableau calculi that exhibit a combination
of features that are often neglected but useful
in the context of inductive theorem proving.
These features include: 
   - dual Skolemization ("raising")
   - explicit treatment of variable dependencies
   - "liberalized" delta-rule
   - preservation of solutions (i.e. intermediate
     subsitutions can always be augmented to 
     final ones)

The central part (in my opinion) is the presententation
of a quite abstract form of the calculi that
can be instantiated to various concrete formats for
proof search.

The ideas involved are less novel as the unfamiliar
terminology seems to suggest. But the connection to
relevant literature is made explicit at various point.

The heavy technical machinery hardly allows for a
"light reading" of the paper. (This is well reflected
in the somewhat baroque - but adequate - title.)
However, otherwise the presentation is fine. 
The examples, as well as many informal remarks are helpful,
probably even essential for most readers.

There are no proofs in this version of the paper. 
But I think that - in this case - this is not
an important issue, for the following reasons:
    - reference to an easily accessible full version is given
    - proofs are rather standard anyway
    - the paper emphasizes a certain combination of
      very clearly presented _concepts_ over new _results_ 
      (in the narrow sense)

For a journal version I would rather like to see
a long paper combining the material on the basic calculi 
(presented here) with the authors results on inductive theorem 
(as in another paper of the author).
However in the given context, I consider the presented paper
interesting and significant enough to warrant publication.