Bernd Loechner and Stephan Schulz: An Evaluation of Shared Rewriting

Abstract:

We present an experimental study on the use of shared rewriting in
equational theorem proving. We identify the main effects that lead to
term sharing in the proof state and experimentally show their
influence.  Besides the analysis of sharing and the _sharing factor_
we gain insights on the benefits for rewriting and matching operations
by a comparison of the theorem provers E and Waldmeister.

This also allows us to conclude that the influence of the side effects
of E's use of shared rewriting on the search process is quite minor.