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

[H. Zantema]

On Mon, 9 May 2005, Frederic Blanqui wrote:

> moment, polynomial interpretations and dependancy pairs have been formalized 
> and proved in color. hence, any proof using polynomial interpretations on 
> dependancy pairs can be formally checked in color. rpo (and perhaps horpo) 
> will be soon added in color. 

Rpo should be added before we really can proceed. How far do you cover
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?


		Best regards, Hans Zantema.

+--------------------------------------+-----------------------------+
|                                      |                             |
|   Dr Hans Zantema                    |   Hoofdgebouw   kamer 6.73  |
|   Faculteit Wiskunde en Informatica  |   tel (040)2472749          |
|   Technische Universiteit Eindhoven  |   fax (040)2468508          |
|   Postbus 513     5600 MB Eindhoven  |   e-mail  H.Zantema at tue.nl  |
|   The Netherlands                    |   www.win.tue.nl/~hzantema  |
|                                      |                             |
+--------------------------------------+-----------------------------+