[Termtools] HofWald 7

[Johannes Waldmann]

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. We need to define a "proof tree"
format. (Matchbox is using a home-brewn tree format for TRS.)
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).

> If you see any other mistake like this, please mail me.

I'd say, in case of doubt, mail this list.
We want an open discussion, and we want it archived,
in order to avoid forgetting or repeating arguments.

I just noticed we *have* a list archive now:
http://lists.lri.fr/pipermail/termtools/
Thanks Claude! I was missing that for a very long time.
This should be helpful when planning for future competitions.

Claude - could you perhaps upload earlier messages to the archive?
I believe "pipermail" can import a standard mailbox-format file.
Assuming, of course, that all list members agree. When the list started,
there was no archive, but I think there was the clear intention
to have one as soon as possible.
-- 
-- Johannes Waldmann -- Tel/Fax (0341) 3076 6479/80 --
---- http://www.imn.htwk-leipzig.de/~waldmann/ -------