Dependency Pairs and Polynomial Path Orders

Martin Avanzini, Georg Moser

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 re…