[Termtools] Re: qualification rounds completed

[Johannes Waldmann]

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

Dear Claude,

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

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

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


Let me recall that at the Nancy meeting, a majority of the
participants expressed
that 1) YES and NO counts should be added, and 2) problems should be
weighted.
You seem to have implemented the weight computation bases on the
current results.
That is fine. Will you also accumulate these weights (per tool) for
the solved problems?

(Of course this is a consideration for preparing the final report,
as this data can be computed after the actual run. Still it would be
nice to have on-line.)
Even if it does not change the outcome of this competition,
I think it shows the direction that we (at least a large part of us)
want the competition to take: encourage development of "interesting"
techniques,
while the clever combination of "standard" (= formerly "interesting")
techniques
should be handled e.g. by agreement on a common control language,
leading to modular provers.


Best regards, Johannes.

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

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