live session at WST, was: Re: [Termtools] belated response

[Johannes Waldmann]

Aart Middeldorp wrote:

>   one might consider running the participating tools
>   on a fairly random selection of TPDB. One can even think of
>   doing this live during a session in the Termination Workshop.

Yes, I remember the first "competition" (at WST 2003 in Valencia)
which was indeed such a live session.

(Each prover running on the respective programmer's notebook.
I don't recall exactly because at that time our focus was string
rewriting. The problems were written on the blackboard,
each programmer typed them in, and raised his hand if his tool produced
a proof. Did we have a working TPDB back then?
There is some information here http://www.lsi.upc.es/~albert/tpdb.html
but there are no exact dates (and no string rewriting problems).
Did we have this before or after the workshop?
Is someone keeping "historical notes"?)

If we do this again, the tools' outputs
should be made visible to all participants,
so perhaps there should only be one computer,
with all provers installed, and output being video-ed to the wall,
and all inputs and outputs logged for later reference.

This does not have to be restricted to TPDB problems,
there could even be "live" submission of problems.

Of course then again we have a technical problem -
we don't want to waste time having an "operator" typing in problems
or running around with USB storage units etc.

But such things can be managed, e. g. if we have a WLAN
in the room and there can be live problem input
(from the participants' computers to the central computer)
via some web interface.

While this could be an interesting WST session
it still is not clear how the results should count
towards the "official" ranking of provers.
-- 
-- Johannes Waldmann -- Tel/Fax (0341) 3076 6479/80 --
---- http://www.imn.htwk-leipzig.de/~waldmann/ -------

_______________________________________________
Termtools mailing list
Termtools at serveur-listes.lri.fr
http://serveur-listes.lri.fr/mailman/listinfo/termtools