[Termtools] TRS-standard[-certified]

[Johannes Waldmann]

> Interestingly enough, there are two proofs where cime3 succeeds
> and AProVE and matchbox don't. Anyone knows why?

Just by scanning the proof:
lexicographic path order, argument filterings?

> I have to admit that I'm not really good at understanding cime3's output.

that's why in the future we should strive to record (on the server)
the abstract proof tree (for Color: the rainbow document -
I guess Cime has a similar proof representation?).

J.W.


-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 257 bytes
Desc: OpenPGP digital signature
Url : http://lists.lri.fr/pipermail/termtools/attachments/20081110/d72530e0/attachment.pgp