In our experiments, we want to assess the power of our new termination method
by running it on a collection of typical TRSs where an inductive argument is needed
for the termination proof.

Note that the computer behind the web interface is slower than the machine used for our experiments and that it is used concurrently by multiple users.

Tool | YES | TIMEOUT |
---|---|---|

AProVE Induction Internal | 16 | 3 |

AProVE Induction ACL2 | 16 | 3 |

In the following tables, each row shows the behavior of *AProVE Induction Internal*
and *AProVE Induction ACL2*
on one example. The entry "YES" means that (innermost) termination of
that example could be proved while "KILLED" indicates that the
tool exceeded the given time limit and was therefore stopped. By clicking
on the respective runtime, one can inspect the output produced by the tool
(including the proof of the theorem prover). To obtain the inputs given
to ACL2, click on "acl" and for ACL2's output on "out".
To load an example into our web interface, just click on the corresponding
button in the first column. Then you can run *AProVE Induction Internal* on the
respective example yourself.

For a similar reason, AProVE also fails on the algorithm *log* where the
termination
argument would be that *half(s(x))* is always smaller than *s(x)*. Again, the
failure is due to the fact that *half* is defined via the selector *p* and a
narrowing on rules instead of dependency pairs would be needed here.

The algorithm *mod* from [Walther 94] computes the modulo operation and
the algorithm *gcd* computes the greatest common divisor. Their main termination
arguments are similar to that of *div*. However, for *gcd*, we have the additional
difficulty that *gcd* exchanges its arguments if the second argument is greater
than the first one. The algorithm *gcd2*
is a variant from [Walther 94] where instead, one always
subtracts the smaller argument from the larger argument. The
algorithm *gcdhard* uses the *mod*-function instead of the *minus*-function in
the recursive arguments of *gcd*.
This last TRS cannot be proved terminating by AProVE,
because essentially, one would have to find a suitable reduction pair which can
conclude that *mod* is less than or equal to both of its arguments, which is
hardly possible with the orderings available in AProVE.

We also investigated the behavior of AProVE on two variants of *maxsort*. In the
TRS *parting04_maxsort_h*, the termination proof is more complicated, since it uses
a recursive identity function *h* in the recursive argument. The algorithm
*maxsortcondition* uses a more natural formulation of the *maxsort* algorithm
with conditions (which however makes the termination proof a bit harder).

Our collection also contains several variants of the quicksort algorithm.
In the TRS *qsort*, the first element of the list is used as pivot
element. Hence, here the main termination argument is that every non-empty
list contains its first argument. In contrast, *qsortlast* takes the last
element of the list as pivot element.
Its main termination argument is that every non-empty
list contains its last argument.
Finally, *qsortmiddle* takes the middle element of the list as pivot element and
its termination argument is that every non-empty
list contains its middle argument. The proof of all these quicksort variants
is possible with AProVE.

The algorithm *parting01_reverse* reverses a list by repeatedly adding
the last element of the list in front. It terminates because every non-empty
list contains its last argument. The TRS *parting02_doublelist* from the TPDB
doubles every number in a list and terminates, since every non-empty
list contains its first argument. The algorithm *zerolist* terminates because of the inductive property that
the subtraction of *x* and *x* always yields 0.