Re: [isabelle] Difficulties with "setsum" (Alfio Martini)



Hi Makarius  and Jasmim,

Even with dont_try0 as a sledgehammer parameter, I get the same old timeout
results both
with Isa2014 and Isa2015-RC1. I havenÂt tried with Isa2015RC2 yet,

Best!.

On Fri, Apr 24, 2015 at 8:10 PM, Makarius <makarius at sketis.net> wrote:

> On Thu, 23 Apr 2015, Alfio Martini wrote:
>
>  My machine (laptop) configuration:
>>
>> Operating System: Windows 8.1, 64-bit operating system
>> Ram Memory: 8GB
>> Processor: intel i5-3230M, 64 bit processor
>>
>
> Fine so far.  It is an up-to-date low-end machine and should work without
> problems, at least in theory.
>
>
>  Lemmas I tried with sledgehammer
>>
>> lemma "[a] = [b] â a = b" oops
>> lemma aux: "m < n+1 âsetsum f {m..n + 1} = setsum f {m..n} + f (n + 1 ::
>> int)"
>> oops
>>
>> When I run the theory file (attached) with Isabelle2015-RC1 I get the
>> following messages in the output window:
>>
>> Sledgehammering...
>>
>>> "remote_vampire": Error: SystemOnTPTP is not available.
>>>
>>> "spass": Timed out.
>>> "cvc4": Timed out.
>>> "z3": Timed out
>>>
>>
> I've tried this with Isabelle2015-RC2.  It is generally better to test
> sledgehammer with these parameters:
>
>   sledgehammer_params [dont_try0]
>
> Doing that, it basically works for me (on 12 cores), but cvc4 breaks down
> as follows:
>
>   SMT: Result:
>     (error "Error in option parsing: option `produce-unsat-cores' requires
> a proofs-enabled build of CVC4; this binary was not built with proof
> support")
>   "cvc4": A prover error occurred:
>   Solver "cvc4" failed -- enable tracing using the "smt_trace" option for
> details
>
> This means there is something wrong with the bundled cvc4 component, and
> Jasmin needs to look at it.
>
>
>         Makarius




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