Superposition calculus: Elimination of redundant atoms

Question

Bachmair and Ganzinger (1991), 'Rewrite-Based Equational Theorem Proving With Selection and Simplification', section 5.2, 'Simplification and Deletion Techniques', page 17, 'Elimination of redundant atoms', discusses the question of when, having used one clause to derive another, you can throw away the first clause instead of ending up with both. As discussed in Redundancy elimination in the superposition calculus you cannot do this in the general case, but you can do it in some particular cases, such as when discarding tautologies or subsumed clauses.

"Let C = Γ, u ≈ v → ∆ be a clause in N. If N |= Γ → u ≈ v, ∆, then N |= Γ → ∆, so that C can be simplified to Γ → ∆. A particular case is the elimination of multiple occurrences of atoms in the antecedent. For example, if C = Γ, u ≈ v, u ≈ v → ∆, then the clause Γ, u ≈ v → u ≈ v, ∆ is a tautology and hence trivially implied by N. Redundant atoms in the succedent can be eliminated in a similar way."

Hang on. "elimination of multiple occurrences of atoms in the antecedent", "Redundant atoms in the succedent can be eliminated" - it would certainly be nice if you could do this, but as I understand it, as discussed in https://stackoverflow.com/questions/29164610/why-are-clauses-multisets you have to treat clauses as multisets, not sets, you cannot just throw away multiple occurrences of the same atom. What am I missing?

And "then the clause Γ, u ≈ v → u ≈ v, ∆ is a tautology" - as I understand it, this is true, a clause which contains both an item and its negation is indeed a tautology and you really can promptly discard tautologies, but what does that have to do with multiple occurrences of the same atom with the same polarity? How is that sentence connected to the rest of the paragraph?

Answer 1

This one seems to be a case of a not very careful choice of notation in this paper.

So we have a clause $C = \Gamma, u\approx v, u\approx v \to \Delta$ in $\mathcal{N}$.

We could use the simplification rule as follows. Let $\Gamma_1 = \Gamma, u\approx v$. Then the following two conditions hold:

1. $C = \Gamma_1, u\approx v \to \Delta$ in $\mathcal{N}$
2. $\Gamma_1 \to u\approx v, \Delta$ is a tautology therefore it can be added to $\mathcal{N}$ without loss of soundness.

Now applying the simplification rule we can replace $C$ with $\Gamma_1\to \Delta$. From the definition of $\Gamma_1$ we have replaced $C$ with the clause $\Gamma, u\approx v\to\Delta$. Effectively the second occurrence of the atom $u\approx v$ has been removed.

They also claim that the same procedure works for removing of multiple occurrences in the succedent.

Also note that this is not specific to equational theorem proving and applies to any atoms.