[Termination tools] Re: termination theorem data base?

[Frederic Blanqui]

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

thanks for your answers hans.

> 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.

i agree with you. for the moment, we do not have enough material in color to 
deal with many current proofs. but i guess that it should be possible in one 
or two years (for TRS's). i formalized the DP theorem in a few weeks. it is 
just a matter of cpu! any volunteer? join color! :-)

> 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

this is exactly what we are looking for! where can we get this data base?