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



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


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