[Termtools] how to handle buggy provers

[Johannes Waldmann]

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

Aart asked:
>
> By the way, what is the current strategy of the organizers
> concerning tools which may have bugs? At SAT competitions, tools
> are moved from "competition" to "demonstration" as soon as a
> problem is found. At earlier termination competitions tools were
> "disqualified" but this year it seems that the tool is simply
> considered not to have been submitted...

(Careful with analogies: most termination provers would be in
"demonstration"
right from the start because for "competition" (in SAT) you'd have to
be open-sourced :-)

Removal of provers was done to avoid the public display of "this
prover has bugs",
which serves no useful purpose.

There's the analogy of not publishing the titles of papers
that have been rejected from a conference/journal.

Of course completely removing a prover also removes the correct proofs
that it may have produced - and that may have used some interesting
new technique
which thereby goes unnoticed. But then, no-one would know which proofs
were correct.

Best regards, Johannes.

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

iD8DBQFGbUs+3ZnXZuOVyMIRAp31AJ9toaShUDsmuw/mj42fXYS/KA9bywCfQ9t6
Brbw/2ntplxC8FR9qq4u968=
=tMdW
-----END PGP SIGNATURE-----