[Termtools] competition, so far - and some remarks on matrices

[Johannes Waldmann]

Dear fellow competitors,

as always it is nice to see the competition running.
Thanks to Claude and Hans for organizing it.
And I'd like to welcome the new participants!


As for TTTbox - I am curious as to its relation to TTT.
Since TTT does not participate, is TTTbox its "successor"?
But TTTbox does not apply TTT's methods (interpretations, DP)?


Then, you may ask what's the difference between the matrix tools
(jambox, matchbox, multum, (and torpa, see below)). I am not
a spokesperson for the group, in fact there is no group, but here
is what I know or heard ... I think the approaches are quite diverse:


jambox: full power

(RFC-mb, labelling, dependency pairs,
matrices from linear programming and SAT solver)


matchbox: restricted

(RFC-mb, labelling,
matrices from linear programming
and SAT solver only for coefficients in {0,1} - the "one bit wonder".
The "wonder" is not complete, I miss SRS/Zantema/z086. But anyway.)


multum: pure

(just matrices, from linear programming
and from a new, direct method, not using any SAT solver)


torpa:

does in fact also use matrices (among many other methods,
of course): a proof step like
   [A] Choose interpretation in NxN,
   order :  (x,y) > (x',y') <==> x > x' & y >= y'
   a : lambda (x,y) . (x+y,4y) , ...
is a matrix interpretation  a = [[1,1,0],[0,4,0],[0,0,1]], ...
I believe Torpa's matrices are found by more or less random guesses
(no dedicated solver).


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