Re: [isabelle] Automating the auto-tools



On 7/21/2012 4:38 AM, Lars Noschinski wrote:
On 21.07.2012 03:39, Gottfried Barrow wrote:
I haven't completely figured out how the continuous prover works. In a
big file, it sometimes seems to go into a dormant state if I don't go
all the way to the bottom and click on the line where the "end"
statement is.

It should process more or less to the point where you are looking at in
the editor. This saves a lot of computing effort, when you are editing
something in the middle of a big theory...

Okay. I guess the general rule is that if some code can be seen in a jEdit view, then the continuous prover will work on the file up to that point.

To belabor the point, I suppose if I had 10 jEdit views open of 10 different .thy files, the continuous prover would try to work on all of them up to the code that could be seen in each view.

That's how it appears. I re-generate the tester file from the theorem. I click back on the jEdit view which has my main file. jEdit asks me if I want to reload the re-generated file. I say yes, and the re-generated tester file gets reloaded in both jEdit windows, and the continuous prover starts working away on the view that shows it. All of the code for the tester file can be seen, so the continuous prover works until it gets to the end.

I broke the two tester theorems into four: Sledgehammer on the theorem. Nitpick on the theorem. Nitpick on the negation. Sledgehammer on the negation.

LEARNING BY ACCIDENT WITH AUTO-TOOLS

By accident, I found out that importing my complete file will allow Sledgehammer and Nitpick to find things they otherwise couldn't find, which makes sense to do for the purposes of trying to find inconsistencies.

Being back in my original file, rather than a simplified version for experimenting, I had the incorrect axiom uncommented out,

  (x IN u <-> x IN v) --> u = v,

instead of the commented correct version,

  !u. !v. (!x. x IN u <-> x IN v) --> u = v

In my main file, I have the theorem stated before another axiom because I don't want the axiom to be used to prove the theorem.

Well, in my tester file, where the negation of the theorem is being tested by Nitpick and Sledgehammer, spass and e found proofs for the negation using my additional axiom, though yices and Z3 didn't.

Lesson? Axioms. You don't want them, which has been addressed. If you use them, be afraid. Very afraid.

Additional lesson? I want to put back in some of those provers to see who can find the inconsistency and who can't.

The prover e tells me:

"The prover found a type-unsound proof ... even though a supposedly type-sound encoding was used (or, less likely, your axioms are inconsistent). Please report this to the Isabelle developers."

We understand that Jasmin or another develop had his peers in mind when he said, "or, less likely, your axioms are inconsistent".

I choose the spass metis theorem. After inserting it, in the output window, it tells me "Metis: the assumptions are inconsistent".

I comment out the wrong formula and un-comment the right formula. The theorem is proved, and nothing else shows up wrong at this point.

Sledgehammer or Nitpick completing their attempts is slowest when I try to disprove what's true, and try to prove what's not true.

Of course, I have the timeouts for both set to 120 seconds.

I need to experiment on Linux under VirtualBox to see what kind of performance I get. I dread setting it all up, and that kind of setup isn't totally trouble free either.

Regards,
GB








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