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

Sascha Böhme boehmes at in.tum.de
Sat Oct 1 22:15:19 CEST 2016

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“.


Von: Makarius
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20161001/19e0bcd0/attachment.html>

More information about the isabelle-dev mailing list