Carsten Fuhs

 

 

Beyond Integer Polynomial Interpretations

 

Abstract:

We present a new approach for termination proofs that uses polynomial
interpretations (with possibly negative coefficients) together with
the "maximum" function. To obtain a powerful automatic method, we solve
two main challenges:

(1) We show how to adapt the latest developments in the dependency pair
framework to our setting.

(2) We show how to automate the search for such interpretations by
integrating "max" into recent SAT-based methods for polynomial
interpretations.

Furthermore, not only can the power of polynomial interpretations be
increased by changing the shape of the interpretation (e.g., by
using the "maximum" function), but also by using interpretations into a
different domain, such as the rationals.

However, searching for such interpretations is considerably more
difficult than for integer polynomials. Hence, we develop new criteria
to decide when to use rational instead of integer polynomial
interpretations. Moreover, we present SAT-based methods for finding
rational polynomial interpretations efficiently.

We implemented our contributions in the termination prover AProVE, and
experimental results show that both approaches lead to further increases
in termination proving power.