[Termtools] modularization

[Johannes Waldmann]

Dear all,

I really want to see a "modularized" competition some day.
That is, provers should be submitted as a combination of modules
(i.e. sub-provers that produce nodes of a proof tree),
and after the competition, modules are *free* for re-use
by anyone.

Then authors could concentrate on developing new modules,
or new combinators for existing modules,
instead of wasting time re-inventing the wheel.
E. g. jambox/SRS obviously has a brilliant loop checker,
so why write your own? Multum uses GLPK to find additive weights.
TTTbox does a clever *-bounds approximation etc.
I think all of these should be available for re-use,
in order to get some advance on a global level.

Of course we need to define an interface (and that's about the
same question as for the proof format). A first step would be
that a prover can, on input R, output a system S
with SN(R) <= SN(S). Or perhaps SN(R) <=> SN(S)?
But the DP method would output a set of systems, etc.

The question then is perhaps how to award prizes in a modularized
competition. Should the credit go to the module author
or to the "combinator" author? I think we should still count
just the number of solved problems, that is, award goes to the
"combinator". If all modules (of the previous years) are free,
then all "combinator" programs have equal chances.
(They can combine the known modules, or add new ones.)
-- 
-- 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