Hi Florian,
I've been testing a lot since Friday.
thank you for doing the work
... demo categories
No competition there (by definition), but still interesting. Tables show some "new results", I'd like to know how these came to be: new method, new implementation, faster CPU, got lucky ... Perhaps the AProVE team can enlighte us (on this list - since we don't have a termination workshop this year) It seems we cannot currently view the actual proof output https://github.com/TermCOMP/starexec-master/issues/109 Best regards, Johannes.
Hey Johannes, The "new results" from the demo categories are not due to new methods or implementation, but just due to the fact that, e.g., for complexity AProVE keeps trying to improve the result until the timeout strikes, so there are some examples, where something happens just before (or after) the timeout. Hence, there are always a few different results every year. There has been some work on termination of term rewriting in AProVE, but mainly in the area of probabilistic and relative termination. E.g., for relative termination we developed a new variant of DPs that I am going to present at IJCAR, which we use in our strategy for relative TRS and also showcase in the relative SRS strategy. Many thanks also from me to Florian for all the work! Kind regards, Jan-Christoph
Dear Jan-Christoph, thanks for explanations.
E.g., for relative termination we developed a new variant of DPs that I am going to present at IJCAR, which we use in our strategy for relative TRS and also showcase in the relative SRS strategy.
sounds great, and I am looking forward to the SRS-relative match ... I stole your idea (seen at termcomp 23) of removing epsilons by context closure. This seems better for matrix interpretations. - Johannes.
participants (3)
-
Florian Frohn -
Jan-Christoph Kassing -
Johannes Waldmann