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.
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.
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.
Combination Procedure. The procedure described here suffers from the same problem as the one described in the FroCoS'2000 submission [BT2000]. See explanation above.