POP* and Semantic Labeling Using SAT

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.

• Type: Journal
• Year: 2009
• Where: ESSLLI
• Authors: Martin Avanzini
• Keywords: Automated Reasoning, ESSLLI 2009, Innermost Runtime Complexity, Polynomial Path Order, Semantic