[Termtools] mopping up ...

[Johannes Waldmann]

Dear all,


the competition is over
http://nfa.imn.htwk-leipzig.de/termcomp-2015/competitions/4
and also the demonstration stage is finishing
http://nfa.imn.htwk-leipzig.de/termcomp-2015/competitions/5

Albert will give a summary talk tomorrow at CADE.
I assume that you can help him by writing comments here,
e.g., on what was the most interesting/surprising
observation/result/method.


E.g., one observation is that there is a focus on lower bounds:

* lower bounds for complexity (RCi) (AProVE got many points there)
http://nfa.imn.htwk-leipzig.de/termcomp-2015/results/complexity/noquery/10312

* a completely new method (using tree automata and SAT)
for TRS/SRS nontermination (AutoNon by Jörg Endrullis)
(see [1] below)

* nontermination for cycle rewriting by two methods:

** transformation (cycsrs by David Sabel and Hans Zantema)
http://nfa.imn.htwk-leipzig.de/termcomp-2015/pairs/121440569

** closure enumeration and some combinatorial analysis
(matchbox - using an "unpublished but important" method)
http://nfa.imn.htwk-leipzig.de/termcomp-2015/pairs/121440639


For browsing this year's results, use "flexible query".
That's the way to isolate, e.g., where you said NO,
but others said nothing:

[1]
http://nfa.imn.htwk-leipzig.de/termcomp-2015/results/standard/Query%20%5BFilter_Rows%20%28And%20%5BAny,Any,Any,Any,Any,Equals%20%22solver-no%22,Any,Any%5D%29,Filter_Rows%20%28And%20%5BEquals%20%22nothing%22,Equals%20%22solver-maybe%22,Equals%20%22solver-maybe%22,Equals%20%22solver-maybe%22,Equals%20%22solver-maybe%22,Equals%20%22solver-no%22,Equals%20%22solver-maybe%22,Equals%20%22solver-maybe%22%5D%29%5D/10257


I will look into making this work for comparison with last year.
At the moment it does not, because benchmark ids for different TPDB
versions are not related. I will see that I can find a work-around
(for using a different key for the tables).


Best regards, Johannes.