Modular Complexity Analysis via Relative Complexity

Below we report on the experiments performed with CaT on the 1172 non-duplicating TRSs in version 7.2 of the TPDB. All tests were performed on a server equipped with eight dual-core AMD Opteron™ 885 processors running at a clock rate of 2.6 GHz on 64 GB of system memory. For all experiments we used a 60 seconds time limit. We remark that similar results have been obtained on a dual-core laptop. In the following direct refers to the conventional setting where all rewrite rules have to be oriented at once whereas modular first transforms the given TRS into a relative TRS before the CP processors from Sections 6 are employed. As base methods we use the match-bounds technique as well as TMIs and arctic matrix interpretations of dimensions one to three. The latter two are implemented by bit-blasting arithmetic operations to SAT. All base methods are run in parallel, but criteria that yield larger derivational complexity are executed slightly delayed. This allows to maximize the number of low bounds.

Experimental Results: results and statistics