[Termtools] Re: qualification rounds completed

[Claude Marché]

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

    Johannes> -----BEGIN PGP SIGNED MESSAGE-----
    Johannes> Hash: SHA1

    Johannes> Dear Claude,

    Johannes> looking at the qualifiying table, the question comes up:
    Johannes> will you be running the competition in "horizontal" or "vertical" mode?

    Johannes> (for qualifiying, you seem to use "for each tool do: for each problem
    Johannes> do:..."
    Johannes> but for competition, swapping the loops would be more interesting?)

This is only for the qualification rounds. For the competition, it
will be the other way around, as usual, plus a new non-deterministic effect: since I
use a multi-processor computer, several tools will run in parallel,
and results may appear in some random order.

    Johannes> and in what order do you plan to run SRS, TRS, LP, FP ?

Indeed FP category is ready to run -> is already started.
I plan to start LP as soon as possible. 

For SRS and TRS, I plan to use different computers, so they will run
in parallel. But they are not ready to start yet.


    Johannes> Let me recall that at the Nancy meeting, a majority of the
    Johannes> participants expressed
    Johannes> that 1) YES and NO counts should be added, 

Done.

     and 2) problems should be
    Johannes> weighted.

Done.

    Johannes> You seem to have implemented the weight computation bases on the
    Johannes> current results.
    Johannes> That is fine. Will you also accumulate these weights (per tool) for
    Johannes> the solved problems?

What does it mean ? A weighted score ? Quite possible to do. I can
even do it after the competition started, since the scores are computed
on the fly when printing the web page.

    Johannes> (Of course this is a consideration for preparing the final report,
    Johannes> as this data can be computed after the actual run. Still it would be
    Johannes> nice to have on-line.)

    Johannes> Even if it does not change the outcome of this competition,
    Johannes> I think it shows the direction that we (at least a large part of us)
    Johannes> want the competition to take: encourage development of "interesting"
    Johannes> techniques,
    Johannes> while the clever combination of "standard" (= formerly "interesting")
    Johannes> techniques
    Johannes> should be handled e.g. by agreement on a common control language,
    Johannes> leading to modular provers.


    Johannes> Best regards, Johannes.

    Johannes> -----BEGIN PGP SIGNATURE-----
    Johannes> Version: GnuPG v1.4.2 (GNU/Linux)
    Johannes> Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

    Johannes> iD8DBQFGY//o3ZnXZuOVyMIRAujDAJ9je854jXI46wS4HjMnlzbIw055oACeMVAU
    Johannes> pAk1VGjKb1SREwjxqku8uUY=
    Johannes> =hBeS
    Johannes> -----END PGP SIGNATURE-----

    Johannes> _______________________________________________
    Johannes> Termtools mailing list
    Johannes> Termtools at lists.lri.fr
    Johannes> http://lists.lri.fr/mailman/listinfo/termtools

-- 
Claude Marché                          | tel: +33 1 72 92 59 69           
INRIA Futurs - ProVal                  | mobile: +33 6 33 14 57 93 
Parc Orsay Université - ZAC des Vignes | fax: +33 1 74 85 42 29   
3, rue Jacques Monod - Bâtiment N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |