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