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

2016-10-01 Thread 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___
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"

2016-10-01 Thread Makarius 
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