Abstract

The polynomial path order (POP* for short) is a termination method that induces polynomial bounds on the innermost runtime complexity of term rewrite systems (TRSs for short). Semantic labeling is a transformation technique used for proving termination. In this paper, we propose an efficient
implementation of POP* together with finite semantic labeling. This automation works by a reduction to the problem of boolean satisfiability. We have
implemented the technique and experimental results confirm the feasibility of our approach. By semantic labeling the analytical power of POP* is
significantly increased.

BibTeX

@inproceedings{MA-ESSLLI08,
  author      = "Martin Avanzini",
  title       = "{POP*} and Semantic Labeling using {SAT}",
  booktitle   = "Interfaces: Explorations in Logic, Language and
                 Computation",
  series      = "Lecture Notes in Artificial Intelligence",
  volume      = 6211,
  pages       = "155--166",
  publisher   = "Springer-Verlag",
  year        = 2010
}