On Implementing Modular Complexity Analysis
Harald Zankl, Martin Korp · EPiC series in computing · 2018
We recall the recent approach by (Zankl and Korp, 2010) to prove upper bounds on the (derivational) complexity of term rewrite systems modularly. In this note we show that this approach is suitable to tighten bounds after they have been established. The idea is to replace proof steps with a large bound by (new) proofs that yield smaller bounds. An evaluation of the approach shows the benefits.