[Termtools] HofWald 7

[Koprowski, A.]

> Cime also proved termination of the standard base
> of combinatory logik CL(S,K,I) (TRS/SK90 - 4.40)
> This is, well, not exactly the orthodox viewpoint.
> 
> To me it shows that we really should work towards the goal
> of automated verification. 
  I'm glad to hear that!

> We need to define a "proof tree"
> format. (Matchbox is using a home-brewn tree format for TRS.)
  That's exactly what CoLoR (http://color.loria.fr) project is trying to
do. There's been an initial discussion on the format of the proof
output. I think soon we should pick up this topic again.

> One potential problem might be that such a proof tree
> represents the result but not the search (but a search trace
> could be output to stderr independently).
  But why would we need a trace of the search? If we want to verify the
correctness of the proof produced by a tool then we need to examine the
proof itself but the way in which it was found is irrelevant for that. 

  Kind regards,
   Adam Koprowski

--
========================================================================
 Adam Koprowski, (A.Koprowski at tue.nl, http://www.win.tue.nl/~akoprows)
 Department of Mathematics and Computer Science
 Eindhoven University of Technology (TU/e)
 The difference between impossible and possible lies in determination
      Tommy Lasorda 
========================================================================

_______________________________________________
Termtools mailing list
Termtools at lists.lri.fr
http://lists.lri.fr/mailman/listinfo/termtools