[Termination tools] termination competition: certification of proofs

[Johannes Waldmann]

I welcome very much the idea of formally verifying
the output of termination provers,
and I agree with everything Hans said.

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?)

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".

Best regards,
-- 
-- Johannes Waldmann -- Tel/Fax (0341) 3076 6479/80 --
---- http://www.imn.htwk-leipzig.de/~waldmann/ -------