[Termination tools] Re: termination theorem data base?

[Frederic Blanqui]

On Tue, 10 May 2005, Juergen Giesl wrote:

> I agree that the idea of checking the proof output formally would be very 
> nice, but I also don't know how easy/realistic this is at the moment. In 
> addition to the problems mentioned I also see the problem that different 
> tools work on different objects. Some tools really work on TRSs, but for 
> example AProVE works on 4-tuples consisting of a TRS, a set of dependency 
> pairs, another TRS to define the evaluation strategy, and a flag. (This is 
> the new so-called "DP framework" from our LPAR04-paper. This framework is 
> meant to combine arbitrary termination techniques and it is much more 
> powerful and flexible than just combining termination techniques in a naive 
> way by applying them repeatedly to the TRS.)
>
> This means that instead of having just a collection of theorems which is 
> used by all tools, instead we might need different theorems for each tool.

the data structures and algorithms you use for implementing the termination 
criteria and the heuristics should not really matter. the input format is the 
same for everyone. so, you should be able to relate your results to some known 
theorems. perhaps, some of your theorems may use other things than just a trs, 
as you mentioned. in other cases, a simple transformation from one 
formalization to another may be required. but, i guess, this can certainly be 
formalized and proved in color too.