[Termtools] SRS standard sub-category

[Johannes Waldmann]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1


>
> Any interesting comments?
I will give some comments on matchbox, jambox, multumnonmulta, torpa
for SRS
(I don't know enough detail about the others): w.r.t. last year,

* jambox did not change

* multumnonmulta added self-labelling but otherwise still applies only
the "direct" matrix method (no DP transform),
  with basically last year's "magic" matrix finder (unique approach,
involves no SAT solver).

* torpa added the matrix method (via SAT), and this should bring it up
to jambox'  performance (roughly);
  and quasi-periodic interpretations (RTA07 paper by Hans and me),
this gives an additional advantage

* matchbox added tropical^H^H^H^H^H^H^H^Harctic matrix method
  which is somehow related to QPI (see my WST paper, on matchbox web
site).
  this explains that matchbox and torpa seem to have roughly similar
score (so far -
  matchbox does use "standard" matrices only for dimension 2, above
it's all arctic,
  this seems to fit well with the "small" SRSs, but   and it will lose
some proofs on SRS/Zantema/ later on)


as noted by Peter, jambox does not seem to be running at full strength.
It used to find 6 loops in SRS/Gebhardt/*, and now there is nothing?
(See other email.)

Speaking of loops, it is nice that we have a dedicated loop finder
(NTI) new on the scene,
also matchbox uses a new loop algorithm (see website)

... and it is regrettable that Innsbruck did not send their new SAT
loop finder (see WST07).
It seems they did not want to risk losing time by failed loop searches.
Well, they could have made a separate submission? (one YES prover, one
NO prover).
(I would even go as far as inviting them to submit this loop finder now,
and Claude could run it separately, time permitting.)


Well, these are just a few random observations.
Best regards, Johannes.

-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.2 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iD8DBQFGZZKD3ZnXZuOVyMIRAsDGAKCf3ETZ/mbla1hu+zZ+NeIQCSSR3ACdGeOq
UMRHjKlcvZiJF/oNioRT6VA=
=zqTy
-----END PGP SIGNATURE-----