[Termtools] timeout for verification: 1 minute

[Johannes Waldmann]

> Some problems  are very hard to certify   [...]

Well, what is the definition of "hard" ...

Something like "proof size", but then that's still
relative to a given set of axioms (built-in in coq)
and theories (e.g. Color, Coccinelle).
I assume that using lemmata from pre-compiled theories (*.vo)
is cheap (coqc needs no time, since they are already checked).

So "hard to certify" termination problems can be made easier
by adding more theorems to Color (or, in fact, just add the statement
of termination of the given problem - Would that be cheating?)

Best regards, Johannes.

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 257 bytes
Desc: OpenPGP digital signature
Url : http://lists.lri.fr/pipermail/termtools/attachments/20081105/a1a60e11/attachment.pgp