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"
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
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and