Re: [isabelle] Bug in Sledgehammer / cvc4



Hi Bohua,

Using 2015/Windows with try methods I get with cvc4:

using Max_ge not_le by blast

Without try methods: by (metis Max_ge leD)

Best!

Best!

On Mon, Jun 22, 2015 at 4:57 PM, Bohua Zhan <bzhan at mit.edu> wrote:

> When I tried sledgehammer on the following theorem:
>
> theorem Max_ge': "finite A â x > Max A â Â(x â A)"
>
> The cvc4 output is:
> Try this: using leD by auto (6 ms).
>
> However, the command does not work. It probably should be
> using Max_ge leD by auto
>
> Best,
> Bohua
>
>


-- 
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
www.inf.pucrs.br/alfio
Av. Ipiranga, 6681 - PrÃdio 32 - Faculdade de InformÃtica
90619-900 -Porto Alegre - RS - Brasil



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.