[Termtools] HofWald 7

[Frederic Blanqui]

On Thu, 15 Jun 2006, Johannes Waldmann wrote:

> > > We need to define a "proof tree" format.
>
> >  That's exactly what CoLoR (http://color.loria.fr)
>  >  project is trying to do.
>
> I thought CoLoR tries to provide (Coq) proofs for theorems
> related to termination. So the proof itself would be a Coq script?
> Or do you plan to have an external format as well?

at the moment, color provides no proof format. but this is part of the
project. i'm currently developping one with students. at the moment, our
prototype can automatically certify termination proofs based on polynomial
interpretations. another student is working on rpo. finally, it should not be
too hard to extend it with dependency pair transformations and filterings,
which are already formalized in color. i expect to release our prototype this
summer. once our (simple) proof format will be available, i expect that
developers of termination provers will try to output proofs in this format in
order to automatically check the correctness of their proofs with coq.

> I think we should have one. This would separate two issues:
>
> a) a termination prover should output a proof tree
>     (inner nodes: transformations, leaves: elementary proofs)
> b) each transformation and elementary proof should be translated
>     into CoLoR so the whole tree can be checked by Coq.

this is exactly what we currently try to do.

> The idea is that we can have (a) even before (b) is ready.
> The proof tree could be checked directly.

you are right but the proof format must be carefully designed in order for
color developpers (or others) to be able to easily formalize those proofs in
some proof assistant. so, i am not sure that it is really useful to define a
format for theorems that are formalized in no proof assistant.

> Of course this would prohibit the use of "new" techniques.
> And we would need agreement on the "node" type.
> E.g. AProVE has quite complex requirements
> (the node type is not just a rewrite system).

i wonder if it is possible... but it is not necessary. the proof format could
allow various node types.

> >   But why would we need a trace of the search?
>
> the tool author wants to know what the program is/was doing,
> and for how long, nothing more.
> I was not suggesting to formalize search traces.

traces and proofs are indeed two different things although traces can be used
to build proofs.

> PS: does the list archive really work? It stops on May 25th?
> (I'm not changing this email's subject so that it will occur
> in the proper thread in the archive)
> --
> -- Johannes Waldmann -- Tel/Fax (0341) 3076 6479/80 --
> ---- http://www.imn.htwk-leipzig.de/~waldmann/ -------
>
> _______________________________________________
> Termtools mailing list
> Termtools at lists.lri.fr
> http://lists.lri.fr/mailman/listinfo/termtools
>
_______________________________________________
Termtools mailing list
Termtools at lists.lri.fr
http://lists.lri.fr/mailman/listinfo/termtools