Re: [isabelle-dev] NEWS: new proof method "argo"
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___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: new proof method "argo"
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 > examples. > > 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? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] NEWS: new proof method "argo"
*** 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 examples. This refers e.g. to Isabelle/ed98a055b9a5. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev