[Termtools] Upcoming competition - discussion during NancyWorkshop

[Koprowski, A.]

>> What if a prover produce directly a checkable proof ?
 Ok, but what if not? If it outputs a directly checkable proof then it's
not a problem as it just outputs the same thing in the final generation
phase.

>> I don't see the point in reading a proof before generating. What if a
>> we think that it is interesting to have an intermediate language for
>> "termination certificates" that any termination prover could output,
>> and from which any termination proof certifier (eg. rainbow) could
>> generate a full formal proof in some safe proof checker/assistant
>> (coq, isabelle/hol, etc.)
> I understand what is such a language and what can be obtained from it,
> btw you know we are designing one.  Still I see no point in making a
> rule of it.
 A point of making such a rule is that we don't want to force
termination provers to output a Coq script but instead a proof in this
language, which then is translated by an appropriate mechanism (like
Rainbow) to a final Coq proof.

>> we also took advantage of this meeting to discuss some aspects of the
>> termination competition.
> These aspects should be discussed on the relevant list, let's thank
> Johannes for posting them.
> > then, this is no problem for you: your checkme command has nothing
to
> > do! :-)
> Thus such a rule is useless, I see you agree. :-)
 It may be useless for tools that want to output formal proof (Cime?)
but it's definitely useful for tools that want to output proofs in the
intermediate format.

   Best wishes,
   Adam

--
========================================================================
 Adam Koprowski, (A.Koprowski at tue.nl, http://www.win.tue.nl/~akoprows)
 Department of Mathematics and Computer Science
 Eindhoven University of Technology (TU/e)
 The difference between impossible and possible lies in determination
      Tommy Lasorda 
========================================================================