[Termtools] Re: SRS standard sub-category

[Peter Schneider-Kamp]

Carsten Otto schrieb:
> On Wed, Jun 06, 2007 at 02:57:51PM +0200, Johannes Waldmann wrote:
>> What is happening in the TRS category meanwhile? Anyone care to comment?
> 
> It is working just fine without comments :)

Which should not preclude anyone from commenting. I'll have a go.

Jambox's performance seems to be seriously disturbed by the
120s limit. That's not nice as we all know it can do much better.

MU-Term's performance is quite respectable. Especially there is
a number of examples (like SchneiderKamp/trs/thiemann10.trs)
which can be handled by rational polynomials (here by interpreting
half as 0.5*x). This is indeed very nice, because without rational
polynomials we can only give proofs using dependency pair
transformations repeatedly.

TTT2 comes in 2nd (probably profiting from Jambox's demise). Besides
an improved labelling, matrix interpretations seem to
use usable rules w.r.t. argument filtering. Thus, they
can handle examples like Schneider-Kamp/trs/kabasci* which.

Finally, AProVE has some small problems with the timing, too.
At home, we can handle approximately 20 more examples on a single
core Pentium 4 at 2.4 GHz within 60s. Otherwise, the Beerendonk
examples (motivated by imperative loops) seem to pose no big
challenge to AProVE. Also it can handle many of the
Schneider-Kamp/trs/otto* and Schneider-Kamp/trs/cade* examples
for termination due to bounded increase.

Kind Regards,
Peter
-- 
Peter Schneider-Kamp   mailto:psk at informatik.rwth-aachen.de
LuFG Informatik II     http://www-i2.informatik.rwth-aachen.de/~nowonder
RWTH Aachen            phone: ++49 241 80-21211