Cesare Tinelli and Calogero Zarba. Combining non-stably infinite theories. 4th International Workshop on First Order Theorem Proving (FTP'03).

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. Cooperation of Background Reasoners in Theory Reasoning by Residue Sharing. International Workshop on First order Theorem Proving (FTP'2000).

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. Combining Equational Theories Sharing Non-Collapse-Free Constructors. Frontiers of Combining Systems (FroCoS'2000).

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. Deciding the Word Problem in the Union of Equational Theories Sharing Constructors. In Proceedings of the 10th International Conference on Rewriting Techniques and Applications (RTA-99), Trento, Italy, 1999. ©Springer-Verlag

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

Last updated: 2003