Termination Tools in Ordered Completion


Ordered completion is one of the most frequently used calculi in equational
theorem proving. The performance of an ordered completion run strongly
depends on the reduction order supplied as input. This talk describes how
termination tools can replace fixed reduction orders in ordered completion
procedures, thus allowing for a novel degree of automation. Our method can
be combined with the multi-completion approach proposed by Kondo and
Kurihara. We present experimental results obtained with our ordered
completion tool omkbTT for both ordered completion and equational theorem
proving.