Exploiting suspected redundancy without proving it
Hari Mony, Jason Baumgartner, Viresh Paruthi, Robert Kanzelman · 2005
We present several improvements to general-purpose sequential redundancy removal. (1) We propose using a robust variety of synergistic transformation and verification algorithms to process the individual proof obligations. This enables greater speed and scalability, and identifies a significantly greater degree of redundancy, than prior approaches. (2) We generalize upon traditional redundancy removal and utilize the speculatively-reduced model to enhance bounded search, without needing to complete any proofs.