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.