Proving Termination of Rewrite Systems using Bounds

Below the results of TTTbox for the 87 non-left-linear TRSs in version 3.2 of the TPDB are accessible. All test were performed on a server equipped with two Intel® Xeon™ processors running at a CPU rate of 2.40 GHz and 2048 MB of system memory. For all experiments we used a 60 seconds time limit. In the first part of the experiments we deal with right-linear TRSs and test for match-raise-boundedness, both with the explicit approach for handling raise rules described in the first paragraph of Section 6 and the implicit approach using raise-consistent tree automata. In the second part we deal with non-right-linear TRSs and test for roof-raise-boundedness. The usage of right-hand sides of forward closures is indicated by rfc.

Experimental Results:

• right-linear TRSs (28 TRSs): results and statistics
• non-right-linear TRSs (59 TRSs): results and statistics