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.
