Dependency Pairs and Polynomial Path Orders
Logic in Computer Science
2011-06-09 v3 Artificial Intelligence
Computational Complexity
Symbolic Computation
Abstract
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.
Cite
@article{arxiv.0904.0981,
title = {Dependency Pairs and Polynomial Path Orders},
author = {Martin Avanzini and Georg Moser},
journal= {arXiv preprint arXiv:0904.0981},
year = {2011}
}
Comments
23 pages, conference version accepted at RTA 2009