[Termtools] HofWald 7

[Johannes Waldmann]

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

The idea is that we can have (a) even before (b) is ready.
The proof tree could be checked directly.
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).

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

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