Abstract

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

BibTeX

@inproceedings{MAGM-RTA09,
author      = "Martin Avanzini and Georg Moser",
title       = "Dependency Pairs and Polynomial Path Orders",
booktitle   = "Proceedings of the 20th International Conference on Rewriting
               Techniques and Applications",
series      = "Lecture Notes in Computer Science",
publisher   = "Springer-Verlag",
volume      = 5595,
pages       = "48--62",
year        = 2009
}