[Termination tools] Re: scaling up SRSs

[Johannes Waldmann]

Claude Marche wrote:

> Of course, I will add your srs encoding the syracuse problem in the
> tpdb !

oh really. do you expect any one of the programs to solve this?
what about adding a TM simulation of some RSA factoring challenge,
or perhaps there is even an encoding of P ?= NP
or the Riemann Hypothesis.

if you want very hard, but provably terminating TMs,
then take Busy Beavers: http://www.drb.insel.de/~heiner/BB/mabu90.html
(the 5 state champion perhaps)?


on a general note, there seem to be
two large classes of (termination) problems:

* so called "real" problems (i. e. they originate from some application
   domain - not term rewriting - like group theory, or (TM) verification)
   (these are the kind of problems that Claude suggests for SRS)

* "artificial" problems that mainly show differences between tools
   (these are typically constructed by the author(s) of one tool
   who know very well the weaknesses of another tool :-)

There should be problems of both sorts in the data base.
-- 
-- Johannes Waldmann,  Tel/Fax: (0341) 3076 6479 / 6480 --
------ http://www.imn.htwk-leipzig.de/~waldmann/ ---------