[Termtools] timeout for verification: 1 minute

[Frederic Blanqui]

By "hard", I think that Julien means that it takes a very long time 
because Coq is slow or the way verifications are done with Coq is optimal.

Johannes Waldmann a écrit :
>> 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.
> 
> 
> 
> ------------------------------------------------------------------------
> 
> _______________________________________________
> Termtools mailing list
> Termtools at lists.lri.fr
> http://lists.lri.fr/mailman/listinfo/termtools