Redundancy elimination in the superposition calculus

Question

When proving theorems with the superposition calculus, we deal with three kinds of rules:

1. Generating rules: from pair of clauses A and B, generate new clause C while keeping the original pair, e.g. superposition in the general case.

2. Rewriting rules: from clause A generate new clause B, e.g. equality reflexivity, equality factoring; superposition with a unit equation can also be regarded as a rewriting rule.

3. Eliminating rules: delete a clause, e.g. subsumption, tautology elimination.

The question is, regarding the second category, can we perform a strict rewrite, replacing the original clause with the new one, or do we have to keep the original as well as the new one? In the case of equality reflexivity it looks like we can do the former, but for equality factoring and superposition with a unit equation it's not immediately clear whether this would preserve completeness.

Is there a general way of knowing which is the case? Or a list of which needs to be done in each case?

Answer 1

a leading implementation of the superposition calculus theorem prover is E. in its description of their technology it states some basic theory & background under Proof Procedure:

E uses the DISCOUNT [DKS97] variant of the given-clause algorithm. The proof state is represented by two sets of clauses, the set P of processed clauses (initially empty) and the set U of unprocessed clauses. Clauses in U are ranked according to a heuristic evaluation function, and are processed in order. Processing will first simplify the selected clause g with all clauses in P, then simplify P with g (moving all affected clauses from P back into U), and then compute all direct consequences between g and P that can be derived using the generating inference rules (superposition, equality factoring, and equality resolution). The new clauses are simplified with respect to P and added to U, g is added to P.

This proof procedure is different from the given-clause algorithm implemented in Otter (and many provers since), which also uses U for simplification. The variant E uses was first popularized by DISCOUNT, but also is at the core of Waldmeister. Vampire and SPASS implement it in addition to their primary algorithm.

so [iiuc] the word "rewriting" may be somewhat a misnomer in the actual implementations of the theorem proving rules, because the original clauses are never "deleted" & always retained in case they can be affected or combined with later derivations. the rewriting "moves" "rewritten" clauses between $P$ and $U$ in both directions.

ie rewriting is basically like an addition of new derived (true) clauses to a list of known true clauses, and the movement between $P$ and $U$ is a strategy to find new true clauses in an efficient way (basically tracking the "frontier" in a mixed depth/breadth search, ordered by the priority function), and $P \cup U$ is the set of known true clauses.

dont know of a ref for this but think that heres the theory on all this. suppose $A \implies B$ and then $A$ was "deleted". it might still be possible to derive $B \implies A$ by other derivations and clauses. in that case it would have no effect. but if its not derivable by other routes, then in theory it could lead to changing a complete problem into an incomplete problem. dont know of a reference that shows this. it could be a doable exercise for the reader to come up with an example.

^{fineprint: taking stab at this question due to lack of other responses. am interested in a really authoritative answer to this question also. there is probably a better one than above but this is the best found so far after some research. suspect the question might be better addressed on say math.se, mathoverflow or TCS.se. also found it hard to come by basic descriptions of these concepts & without heavy specialized jargon.}