Setup

This website contains the experimental results for the PhD thesis Derivational Complexity Analysis Revisited.

All Experiments have been performed on a machine with 8 Dual Core AMD Opteron 885 processors and 64GB RAM running Linux. The testbed we used is based on version 8.0 of the termination problems database (TPDB); we used the same restrictions on it as the complexity category of the annual international termination competition used to obtain the basic set of TRSs from which the competition problems are (randomly) selected: we filtered out duplicate instances of the same TRS (modulo strategy), and removed all TRSs with relative rewriting problems, conditional rules, or theory annotations, resulting in this testbed. Moreover, for our experiments with direct techniques whose applicability implies polynomial derivational complexity, we additionally removed all duplicating TRSs, since the derivational complexity of any duplicating TRS is trivially at least exponential. This further restriction resulted in this testbed.

The following software tools were the subjects of our tests: We used version 1.8 of TCT using this configuration file, the final version of cdiprover3 called by this shell script, and version 1.07 of TTT2 using this configuration file (which is based on the configuration file included in version 1.07 of TTT2).