[isabelle-dev] NEWS: new proof method "argo"
makarius at sketis.net
Sat Oct 1 14:07:38 CEST 2016
On 29/09/16 21:44, Sascha Boehme wrote:
> *** HOL ***
> * New proof method "argo" using the built-in Argo solver based on SMT technology.
> The method can be used to prove goals of quantifier-free propositional logic,
> goals based on a combination of quantifier-free propositional logic with equality,
> and goals based on a combination of quantifier-free propositional logic with
> linear real arithmetic including min/max/abs. See HOL/ex/Argo_Examples.thy for
> This refers e.g. to Isabelle/ed98a055b9a5.
This looks very interesting.
How does it relate to "smt" (with Z3 in the back), concerning
performance and problem classes that can be solved?
Concerning the name "argo", is the a relation to "alt-ergo"?
For the coming release, there is still the question what to do with
"old_smt". Shall we remove it now? Or declare it more explicitly as
legacy and remove it later?
More information about the isabelle-dev