  We show how polynomial path orders can be employed efficiently in conjunction
with weak innermost dependency pairs to automatically certify polynomial
runtime complexity of term rewrite systems and the polytime computability of
the functions computed. The established techniques have been implemented and we
provide ample experimental data to assess the new method.

Logic in Computer Science;Artificial Intelligence;Computational Complexity;Symbolic Computation