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