Match-Bounds with Dependency Pairs for Proving Termination of Rewrite Systems

Below we report on the experiments we performed with TTT2 on the 1321 TRSs in version 4.0 of the TPDB that fulfill the variable condition. All tests were performed on a workstation equipped with an Intel® Pentium™ M processor running at a CPU rate of 2 GHz and 1 GB of system memory. For all experiments we used a 60 seconds time limit. Besides the recursive SCC algorithm and the improved estimated dependency graph processor, we use the following four DP processors:

s	the subterm criterion
p	polynomial orderings with 0/1 coefficients
b	the DP processor of Theorem 2 extended to non-left-linear TRS
d	the DP processor of Theorem 10 for left-linear TRSs and the one of Theorem 19 for non-left-linear TRSs

For the latter two, if the DP problem is non-duplicating we take e = match. For duplicating problems we take e = roof for b and e = top for d. Furthermore, the usage of right-hand sides of forward closures is indicated by rfc and the usage of usable rules is indicated by ur.

Experimental Results: results and statistics