[Termination tools] termination theorem data base?

[H. Zantema]

On Mon, 9 May 2005, Frederic Blanqui wrote:

> On Mon, 9 May 2005, H. Zantema wrote:
> > 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.

My impression is that it is still a long way to go to check typical AProVE,
TTT and CiME proofs. Probably (Adam agrees...) checking TPA proofs will
be simpler. I think the same holds for TORPA and TEPARLA. Matchbox
and Jambox have the property that all proofs are based on very few basic
theorems, for which I guess formal checking would be not trivial but 
feasible.

May be the following would be a good idea: apart from  TPDB  we have
TTDB: the termination theorem data base. Here all theorems are collected 
that are useful for automatically proving termination. For the next
termination competition for all generated termination proofs it is mandatory 
to refer to the corresponding theorems in TTDB. This is not a lot of extra
work for the tool developers: only the theorems used in the generated proofs
should be submitted to TTDB, and appropriate references should be added
in the generated proofs. It could also be mandatory to include (references 
to) a proof for every theorem submitted for TTDB; it is reasonable that one 
does not want to use theorems that have not been proven. Then this TTDB could
serve as an agenda for the CoLoR project. But apart from the CoLoR project 
this new rule would be helpful in itself to get more reliable and readable 
generated proofs: now from the generated proofs it is often not exactly 
clear which underlying theorems were applied. Forcing the tool developers
to formulate exactly all underlying theorems will be helpful to avoid 
errors.
 
		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  |
|                                      |                             |
+--------------------------------------+-----------------------------+