Polynomial Interpretations with Negative Coefficients - Artificial Intelligence and Symbolic Computation - page 195

we determine whether α ( Q ) 0 for all assignments α by checking whether Q ∈

α ∗ ( P 0 ). If Q is non-negative then we certainly have Q ) 0 for all assignments α

and thus follows from Corollary 17. If non-negativeness cannot be shown

then we apply the previous lemma to replace an abstract variable that occurs
only in the negative part of

s N t

Q is tested for non-

Q . The resulting polynomial

α ∗ ( Q )

negativeness. If the test succeeds then for all assignments α we have 0

α ∗ ( and thus also 0 by the previous lemma. According to Corollary 17 this

is sucient to conclude

Q )

s N t

. Otherwise we repeat the above process with
Q . The process terminates when there are no more abstract variables left that
appear only in the negative part of the current polynomial.

5 Experimental Results

We implemented the techniques described in this paper in the Tyrolean Termina-
tion Tool [14]. We tested 219 terminating TRSs and 239 innermost terminating
TRSs from three different sources:

- all 89 terminating and 109 innermost terminating TRSs from Arts and
Giesl [2],
- all 23 TRSs from Dershowitz [7],
- all 116 terminating TRSs from Steinbach and Kuhler [20, Sections 3 and 4].

Nine of these TRSs appear in more than one collection, so the total number
is 219 for termination and 239 for innermost termination. In our experiments
we use the dependency pair method with the recursive SCC algorithm of [12]
for analyzing the dependency graph. The recent modular refinements mentioned
after Theorem 12 are also used, except when we try to prove (full) termination
with the approach of Section 4 (but when the TRS is non-overlapping we do use
modularity since in that case innermost termination guarantees termination).
All experiments were performed on a PC equipped with a 2.20 GHz Mobile Intel
Pentium 4 Processor - M and 512 MB of memory.
Tables 1 and 2 show the effect of the negative constant method developed in
Section 3. In Table 1 we prove termination whereas in Table 1 we prove innermost
termination. In the columns labelled we use the natural interpretation for

certain function symbols that appear in many example TRSs:

n

0 Z =0 1 Z =1 2 Z =2 ···

s Z ( x x x, y x y × Z ( x, y xy

)= +1 + Z ( )= + )=

p Z ( x x −

1 1

− Z ( x, y x − y

1

)= )=

For other function symbols we take linear interpretations

f Z ( x 1 ,...,x n )= a 1 x 1 + ··· + a n x n + b

1 In Tables 1 and 2 we do not fix the interpretation of p when − 1 is not included in
the indicated constant range and the natural interpretation of − is not used.