Sciweavers

AISC
2008
Springer

Search Techniques for Rational Polynomial Orders

13 years 7 months ago
Search Techniques for Rational Polynomial Orders
Polynomial interpretations are a standard technique used in almost all tools for proving termination of term rewrite systems (TRSs) automatically. Traditionally, one applies 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 tackle 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. Topics. computer algebra systems and autom...
Carsten Fuhs, Rafael Navarro-Marset, Carsten Otto,
Added 12 Oct 2010
Updated 12 Oct 2010
Type Conference
Year 2008
Where AISC
Authors Carsten Fuhs, Rafael Navarro-Marset, Carsten Otto, Jürgen Giesl, Salvador Lucas, Peter Schneider-Kamp
Comments (0)