Andreas Schnabl

Experiments with the cdiprover implementations

Below, we list several test results for the three implementations of cdiprover. The experiments mentioned below were done with the known terminating part of the tpdb-4.0. That archive can be obtained here. We have conducted tests single-threaded on a server equipped with 8 AMD Opteron 2.8 GHz dual core processors with 64GB of RAM, and on a 2.40 GHz Intel Core 2 Duo with 2 GB of memory. The test results mentioned below were obtained on the former architecture.

Cdiprover/cdisolver: the list of TRSs which are shown terminating by the combination of these two tools
Test results comparing the performance of cdiprover2 and cdiprover3
Test results checking the benefits of increasing the upper bound on coefficient variables when searching Delta-restricted interpretations with cdiprover3
Test results checking the benefits of increasing the upper bound on coefficient variables when searching Delta-linear interpretations with cdiprover3
Test results comparing delta-restricted interpretations by cdiprover3 with other termination proof methods which imply a quadratic upper bound on the derivational complexity of a given TRS
An examination of the performance of cdiprover3 on the TRS family a(b(x)) -> b^k(a(x))

Downloads

You can download the following cdiprover implementations (Linux-x86 executables, native compiled OCaml, last updated on May 9, 2008):

cdiprover (readme) - this program generates a linear polynomial interpretation, and generates a number of "stubs" for context-dependent interpretations. The stubs are generated according to the heurstic shown in the examples of Hofbauer's paper about context-dependent interpretations [1].
cdiSolver (readme) - this program takes as input one of the stubs generated by cdiprover, and tries to complete it such that the resulting context-dependent interpretation implies termination of the given rewriting system. The constraints which occur when constructing the parameter functions and checking compatibilty are solved using Mathematica. Due to the experimental results mentioned above, development of cdiprover and cdiSolver has been discontinued.
cdiprover2 (readme) - Cdiprover2 searches for context-dependent interpretations using the adapted algorithm of Contejean et al., which is described in [3]
cdiprover3 (readme) - Cdiprover3 is an improved version of cdiprover2, which uses a SAT encoding in order to solve the final Diophantine constraints instead of following the Diophantine constraint solving algorithm described in [2].

References

[1] Hofbauer, D.: Termination proofs by context-dependent interpretations. In: Proc. 12th RTA. Volume 2051 of LNCS. (2001) 108–121
[2] Contejean, E., Marché, C., Tomás, A. P., Urbain, X.: Mechanically proving termination using polynomial interpretations. JAR 34 (2005) 325–363
[3] Moser, G. and Schnabl, A.: Proving Quadratic Derivational Complexites using Context Dependent Interpretations. Draft, available here.