[Termtools] complexity categories

[Johannes Waldmann]

Dear all, and especially dear complexiticians -


looking at the test runs,
there is still some breakage in the complexity categories
(w.r.t. the 2015 syntax http://cbr.uibk.ac.at/competition/rules.php )


TCT3's parser seems broken
http://nfa.imn.htwk-leipzig.de/termcomp-devel/pairs/116633940


aprove sometimes says  WORST_CASE(Omega(O(1)), ?)
http://nfa.imn.htwk-leipzig.de/termcomp-devel/pairs/116633926
perhaps it should be "WORST_CASE(Omega(n^0),?)"
but that's not in the grammar, as the degree must be non-zero (but why?)


aprove sometimes says  YES(O(1), O(n^2))
http://nfa.imn.htwk-leipzig.de/termcomp-devel/pairs/116634239
it should be WORST_CASE(....) ? this is for a certified category,
but I thought certification does not change the format of the answer.


I know, matchbox also says YES(...,...) at the moment.


how would CeTA check that the (ASCII) claim (before the proof)
corresponds to the statement in the proof? does it have this lower
bounds stuff at all? This (still) looks like polynomial upper bounds
only:
http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/IsaFoR/file/ac7531b94e57/IsaFoR/Proof_Checker/CPF_Parser.thy#l1033


So far, I did not update postprocessors because other matters
were more pressing - and I am waiting for your pull requests.
This looks promising: https://github.com/alpako/ceta-postproc ,
does it work? Of course, also the new scoring needs work, around here:
https://github.com/jwaldmann/star-exec-presenter/blob/master/Presenter/Processing.hs#L106


- Johannes.


PS: "and NON_POLY refers to an unspecified exponential" -
is  n \mapsto n^{\log n}  POLY  or  NON_POLY  then?