**Proposition 6.4.**
The proposition's claim is false.
The (polynomial) procedure given in Figure 1 *does not*
compute *mincard(&Gamma)*.
In fact, as proven in a later paper,
the computation of *mincard* is NP-hard.

Cesare Tinelli.

**Proposition 2.**
The claim is not correct as stated.
The sentence
``there is a disjunction &psi of ground literals ...''
should read
``there is a conjunction &psi of disjunctions of ground literals ...''

**Proposition 1.**
Similarly to Proposition 2,
&psi should be a conjunction of disjunctions of literals.

**Theorem 1.**
The completeness argument given for the theorem
is incorrect as stated because it appeals to
the incorrect version of Proposition 2.
However,
it can be easily adapted to use the correct version of the proposition.
The key fact is that
a formula φ_1 & φ_2 & ... & φ_n
(where each φ_i is a disjuntion of literals)
is a residue if and only if
each φ_i is a residue.

Franz Baader and Cesare Tinelli.

**Combination Procedure.**
Contrary to what claimed in the paper,
and because of an oversight in the completeness proof,
the procedure is not complete.
As presented,
it will not recognize the equivalence of two pure terms
which have different signatures
but are both equivalent to a term in the shared signature.

This problem has been fixed in the version of the paper submitted for
journal publication [BT99a].
It was enough to add a new identification rule to deal with
the case above.

Franz Baader and Cesare Tinelli.

**Combination Procedure.**
The procedure described here suffers from the same problem as
the one described in the FroCoS'2000 submission [BT2000].
See explanation above.