[Termination tools] Re: scaling up SRSs

[Claude Marche]

>>>>> "Johannes" == Johannes Waldmann <waldmann at imn.htwk-leipzig.de> writes:

    Johannes> Claude Marche wrote:
    >> Of course, I will add your srs encoding the syracuse problem in the
    >> tpdb !

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

I want such examples in the database too, for the same reason I want
to have non-terminating examples. If a tool answers YES or NO
on the syracuse system, we will have to investigate: it is likely that
this tool have bugs. 

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


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

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

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

    Johannes> There should be problems of both sorts in the data base.

Yes. Please send examples !

-- 
| Claude Marché           | mailto:Claude.Marche at lri.fr |
| LRI - Bât. 490          | http://www.lri.fr/~marche/  |
| Université de Paris-Sud | phoneto: +33 1 69 15 64 85  |
| F-91405 ORSAY Cedex     | faxto: +33 1 69 15 65 86    |