John, something that convinced me that miz3 wants to be strong was stimulated
by Josef, who got the FOL prover Vampire to give 1-line proofs of almost all of
my Tarski miz3 results. Eventually I tried doing the same in miz3, and I'm
including my biggest success below. In about 2 hrs on my fastest machine, with
a MESON solved at number of over a million, miz3 verified a 1-line proof, where
my real proof is 8 lines long and took me quite a long time to come up with.
That's good evidence that even though miz3 may not be super-powerful, it's not
trying to be weak.
Josef, it sounds like you're saying that Mizar is intentionally weak, and that
the reason for weakness is to make it practical to make calls to the huge Mizar
library. And so presumably if you make improvements in library calls, then
Mizar would want to become stronger. Is that right? One thing I can't
understand is how Mizar weakens itself in the first place. Miz3 is as strong
as MESON once you take Freek's constant advice and raise the timeout. I don't
know much about proof assistants, but it's hard for me to see how Mizar can be
doing anything that different, and you seemed to say it yourself: [Mizar's] own
"MESON" - "by".
--
Best,
Bill
horizon := 0;;
timeout := 8000;;
new_type("point",0);;
new_type_abbrev("point_set",`:point->bool`);;
new_constant("Line",`:point_set->bool`);;
let I1 = new_axiom
`! A B. ~(A = B) ==> ?! l. Line l /\ A IN l /\ B IN l`;;
let BiggerThanSingleton_THM = thm `;
let p be A->bool;
let x be A;
assume x IN p [H1];
assume ~(p = {x}) [H2];
thus ? a . a IN p /\ ~(a = x)
by H1, H2, SING_SUBSET, SUBSET_ANTISYM, SUBSET, IN_SING`;;
let Line01infinity2_THM = thm `; :: solved at 175,311,305
let X be point;
let l m be point_set;
assume Line l /\ Line m [H0];
assume ~(l = m) [H1];
assume X IN l /\ X IN m [H2];
thus l INTER m = {X}
by H0, H1, H2, IN_INTER, BiggerThanSingleton_THM, I1`;;
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
