[isabelle-dev] NEWS: new proof method "argo"

[Sascha Böhme]

Hi Makarius,

Compared to „argo“ the „smt“ method is more powerful since it supports quantifiers as well as linear natural and integer arithmetic. For the moment, argo is not capable of proving problems that require both equality reasoning and linear real arithmetic. This combination of theories is no problem for „smt“.

I would mark „old-smt“ as legacy for the coming release and remove it right after the release fork. Please also consider Jasmin’s opinion on this case.

Indeed, the names sound similar, but this is a coincidence as there is no relation to „alt-ergo“.

Cheers,
Sascha

Von: Makarius
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20161001/f8c52e14/attachment.html>