[Termination tools] termination competition: certification of proofs

[Frederic Blanqui]

On Mon, 9 May 2005, Johannes Waldmann wrote:

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

color is indeed built on coq. hence, you could directly output some coq terms 
to express your termination proof wrt the color formalization. but i do not 
think that this is the best way to proceed. as explained by hans, termination 
proofs are combinations of basic theorems (that can be represented by names), 
and require witnesses like polynomials, precedences, etc. so, it does not 
require a syntax as complicated as the one of coq. furthermore, coq or color 
themselves will evolve, while the grammar of termination proofs should 
certainly be stable once it will be defined (even though it will be extended 
from time to time with new criteria). finally, although coq is very nice, some 
people may be interested in using other proof assistants. so, it seems better 
for every body to have an independant format for proofs.

> PS: if we really, really want a separate "proof format", then please
> let's use some XML schema to avoid "concrete syntax wars".

if every one agrees, we can clearly use some xml schema.