[Termtools] TRS-standard[-certified]

[Peter Schneider-Kamp]

Johannes Waldmann wrote:
> TRS-Standard is done, and we have Aprove getting more proofs than TTT2
> than Jambox, both for number of YES and number of NO.

We missed 1000 by 5 examples :)

> Right now category TRS-Standard-Certifying is starting
> (where we'll finally have the "Coccinelle vs. Color" showdown :-)

So far, when using AProVE as a backend, there is no difference
in using Cocinelle vs. Color.

Interestingly enough, there are two proofs where cime3 succeeds
and AProVE and matchbox don't. Anyone knows why? I have to
admit that I'm not really good at understanding cime3's output.

Best regards,
Peter
-- 
Peter Schneider-Kamp   mailto:psk at informatik.rwth-aachen.de
LuFG Informatik 2      http://verify.rwth-aachen.de/psk
RWTH Aachen            phone: +49 241 80-21211