Sciweavers

Share
ESSLLI
2009
Springer

POP* and Semantic Labeling Using SAT

9 years 2 days ago
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.
Martin Avanzini
Added 17 Feb 2011
Updated 17 Feb 2011
Type Journal
Year 2009
Where ESSLLI
Authors Martin Avanzini
Comments (0)
books