[Termtools] competition - (preliminary) results

[Johannes Waldmann]

Dear all,

now the first stage of the Standard TRS category seems finished,
with Aprove slightly ahead of Jambox. Congratulations to both.

Perhaps the authors could comment on the difference between the provers?
What would be the "combined" score (i. e. if Aprove had Matrices,
or if Jambox had ... what exactly? Size change principle perhaps)?

I'd like to congratulate TTTbox (Martin Korp) - it has a strictly
better (than Matchbox) implementation of the match/roof-bound method.
Progress in that area is very welcome.

Also I think it is quite interesting that TPA and Jam/Matchbox
sometimes do "agree" in the sense that TPA finds an integer labelling
while Jam/Matchbox finds matrices. This is certainly related.


(PS: I'll send two more short emails with comments
but I want them as separate threads in the archive.)

Best regards,
-- 
-- Johannes Waldmann -- Tel/Fax (0341) 3076 6479/80 --
---- http://www.imn.htwk-leipzig.de/~waldmann/ -------

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