POP* and Semantic Labeling using SAT

Martin Avanzini

Interfaces: Explorations in Logic, Language and Computation, Lecture Notes in Artificial Intelligence 6211, pp. 155 – 166, 2010.


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.


  PDF |    doi:10.1007/978-3-642-14729-6_12  |  © Springer


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
Nach oben scrollen