Re: [isabelle] A few questions about Isabelle2013



On Sat, 12 Jan 2013, Gottfried Barrow wrote:

SMT PROOFS DON'T RUN THAT RAN BEFORE, AND SLEDGEHAMMER WAS FIRST HAVING PROBLEMS

I saw on the developers list that SMT causes problems, so that answered my question about whether I should use SMT proofs. The reason I had a couple is because they were about 4 times faster than the metis proofs that were found.

You need to be more specific about the kind of problems you throw at SMT/Z3.


Sledgehammer wasn't working correctly at first. It wasn't updating the output window. It was possibly related to me trying to run it on the theorems that had the SMT proofs that didn't work anymore. At some point, after trying different options on different theorems, Sledgehammer started working.

Can you explain this further, beyond the "works for me state"? Was it just confusion about slightly changed options and editor reactivity, or a genuine problem to be isolated?


	Makarius





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