Search Techniques for Rational Polynomial Orders

Authors

Carsten Fuhs, Rafael Navarro-Marset, Carsten Otto, Jürgen Giesl, Salvador Lucas, and Peter Schneider-Kamp

Abstract

Polynomial interpretations are a standard technique used in almost all tools for proving termination of term rewrite systems (TRSs) automatically. Traditionally, one uses interpretations with polynomials over the naturals. But recently, it was shown that interpretations with polynomials over the rationals can be significantly more powerful. However, searching for such interpretations is considerably more difficult than for natural polynomials. Moreover, while there exist highly efficient SAT-based techniques for finding natural polynomials, no such techniques had been developed for rational polynomials yet. In this paper, we solve the two main problems when applying rational polynomial interpretations in practice: (1) We develop new criteria to decide when to use rational instead of natural polynomial interpretations. (2) Afterwards, we present SAT-based methods for finding rational polynomial interpretations and evaluate them empirically.