[Termination tools] termination theorem data base?

[H. Zantema]

On Tue, 10 May 2005, Johannes Waldmann wrote:

> (Hans:)
> 
> >> 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. 
> 
> (Frederic:)
> 
> > this is exactly what we are looking for! where can we get this data base?
> 
> For instance from pages 181 - 259 of TeReSe (ISBN 0 521 39115 6)
> (Chapter 6 "Termination" by Hans Zantema).
> 
> It would make perfect sense to accept everything that's written there
> (that was one purpose of writing that book, I guess)
Indeed this was one purpose. But we should realize that a LOT has happened
since that text was finished some 5 years ago (although the book appeared
not earlier than 2003): e.g., usable rules, polynomials with negative 
coefficients, match bounds, relative termination. In particular a lot has 
been done wrt dependency pairs, which is treated only very shallow in the 
TeReSe book.

My guess is that many variants of basic theorems are used in the generated
proofs, and that the full list of all theorems will be quite substantial.

> and to require that tool authors provide formal statements
> (and proofs, in due course) for what they want to use beyond that.
> (And I accept that challenge for Matchbox.)

Great! For T*A I am quite sure that by the next competition we can have 
references to all applied theory. How about CiME, TTT and AProVE: is all
theory used in generated proofs accessible? This may be in published
papers, in technical reports, or even personal notes available via
home pages.
 
One problem may be that people do not want to make their new techniques 
public before the competition, in order to avoid that they also will be 
implemented in one of the other tools before the competition. This can be 
solved by choosing the deadline for submitting (references to) new theorems 
to be the same as the deadline for the final versions, just as was done 
for the secret problems.


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