[Termination tools] Re: termination theorem data base?

[Juergen Giesl]

Dear all,

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.

Best Regards
Juergen