[Termination tools] termination competition: certification of proofs

[Koprowski, A.]

   Dear all,
 If I may add few words as a person involved in CoLoR project and author
of TPA - tool that took part in this year's competition.

> Let me suggest to avoid a new format for proofs.
> Instead we could perhaps use some existing proof checker format
> (e.g. PVS, Coq) and "just" require that the tools output
> a proof that can then be mechanically verified.
> (Does CoLoR define a new format? It is built on Coq?)
 CoLoR is indeed being developed in Coq. But the idea of proposing the
output format for termination proofs comes from the fact that it's hard
to imagine that authors of all tools would produce Coq scripts
validating their proofs. Instead a more high-level format should be
suggested and then its transformation to Coq proof would be CoLoR's job.
Then every tool that could produce its output in this common format
could get certification for free.
 
> The "basic theorems" would have to be made available
> as sub-procedures (or whatever the proof checker provides).
> It is even conceivable, as a first step,
> that some of the "basic theorems" will be used formally unproven
> (i. e. they are used "as axioms" - sure the proof checkers
> have a way to allow this). That way, we can separate
> "interface" from "implementation".
> PS: if we really, really want a separate "proof format", then please
> let's use some XML schema to avoid "concrete syntax wars".
  XML is fine as far as I'm concerned but let's wait for Frederic's
opinion.
  But then the goal is to come up with the XML schema. For that I see
another problem not mentioned so far, namely that it's not only about
the choice of used "building blocks" (ie. basic theorems) but also about
their precise shape. As far as I know different tools use different
variants of commonly known theorems (dependency pair transformation is
the best example). This format should somehow try to capture all of them
and that's why the more authors of the tools involved in work on this
format the better.

  On the practical side: within CoLoR project so far polynomial
interpretations, dependency pairs and recursive path orderings (on the
way) has been formalized. It's true that not formalized theorems can be
introduced as axioms at the time being but that's why agreeing on common
proof format is so important: it can help find most important missing
theorems and then can stimulate CoLoR team to fully formalize them.

  If there are no other volunteers I can try to propose a (preliminary)
format that would be suitable for TPA. It could serve as a starting
point for extension/discussion.

  Kind regards,
   Adam Koprowski

------------------------------------------------------------------------
-
- Adam Koprowski  (A.Koprowski at tue.nl)
-
- Department of Mathematics and Computer Science
-
- Technical University Eindhoven (TU/e)
-
-
-
- The difference between impossible and possible lies in determination
-
-      Tommy Lasorda
-
------------------------------------------------------------------------
-