[Termtools] supplementing the competition input format

[Johannes Waldmann]

I very much welcome the idea of a common exchange format
for sub-problems that occur in typical (DP) termination proofs.

Together with a common "control language",
this will allow us to compare and combine parts of provers.

This will ultimately make the competition more attractive
because then each participant can concentrate on developing
really new stuff and does not waste time re-inventing wheels.

Maybe the "right" solution would be to use some kind of
XML format (which will be needed anyway for Color/Rainbow:
what is the node type in a proof tree?)
but I think an extension of the TPDB format is fine for now.

I don't know whether QRESTRICTION is "typical" (or "Aprove centric"),
but I do think it is the right idea that Aprove outputs such
QRESTRICTION statements. If a prover does not understand this,
it just ignores them.
-- 
-- Johannes Waldmann -- Tel/Fax (0341) 3076 6479/80 --
---- http://www.imn.htwk-leipzig.de/~waldmann/ -------