Dependency Pairs and Polynomial Path Orders

Martin Avanzini and Georg Moser

Proceedings of the 20^th International Conference on Rewriting Techniques and Applications (RTA 2009), Lecture Notes in Computer Science 5595, pp. 48 – 62, 2009.

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.

  PDF |    doi:10.1007/978-3-642-02348-4_4  |  © Springer

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
}