On Implementing Relative Complexity


We recall the recent approach from (Zankl and Korp, 2010) that allows to
combine different criteria to prove polynomial upper bounds on the
derivational complexity of rewrite systems. In contrast to the question of
termination, which is a plain yes/no problem, the question of the
(derivational) complexity of a rewrite system is more fine-grained. Hence a
complexity prover should not stop as soon as it managed to obtain an upper
bound but try to tighten this bound. We show that the mentioned approach
allows to achieve this goal.