[Termtools] LOAT?

[Florian Frohn]

Dear Akihisa,

LoAT can prove lower complexity bounds and, as a special case of that,
non-termination, but it cannot prove termination. In the complexity
category, it is serving as backend for AProVE, but in the
non-termination category, it is competing on its own.

As it was originally designed for complexity analysis, the default
output (in case it fails to prove anything interesting) is
WORST_CASE(Omega(0),?) instead of MAYBE.

So everything is fine as it is.

Best
Florian


On 25.06.20 06:45, Akihisa Yamada wrote:
> Dear Florian,
> 
> loat seems producing bounds instead of
> YES. https://www.starexec.org/starexec/secure/details/pair.jsp?id=487097787
> 
> Did you intend to participate in the complexity category?
> 
> Best,
> Akihisa
> 
> _______________________________________________
> Termtools mailing list
> Termtools at lri.fr
> http://lists.lri.fr/cgi-bin/mailman/listinfo/termtools
>