[Termination tools] Re: termination competition: certification of proofs

[Frederic Blanqui]

On Mon, 9 May 2005, H. Zantema wrote:

i added color in cc. this is the mailing list of color's users.

> Rpo should be added before we really can proceed. How far do you cover

rpo should be available in a few weeks now.

> dependency pairs? As far as I know even the simple dependency pairs proofs
> (as generated by AProVE, TTT and CiME) compute an approximation of the
> dependency graph, analyze strongly connected components, do something like
> argument filtering, find polynomials for which some dependency pairs
> are strict and some others are non-strict, and then proceed by a new
> dependency graph. For instance, look at the results for TRS/AG01 - #3.15,
> one of the first in the TRS results in the standard term rewriting category.
> Can these proofs (e.g. the TTT proof) fully be checked by CoLoR?

at the moment, we only have the basic dependancy pairs theorem, with no graph 
analysis. yes, we clearly have to add this aspect in color to check these 
proofs.