Michael, this is a discussion of motivation. My desire is for miz3 to become stronger, so I can take bigger inference leaps that will take less time. That would be pointless if John & Freek's desire was that miz3 be ``less able to prove goals,'' as you did not quite say. So I've tried to argue that John & Freek had no such desire. Freek clarified my point:
[...] the main point was that if an inference is _not_ correct, often MESON will run for the full timeout time. So checking proofs with errors (= all proofs when you're not finished yet) gets very slow, and without timeout close to infinite. The timeout thing is just to deal with that. This is especially important for beginners. I still make plenty of errors, but they are errors that I understand, thanks to Freek's private lessons. When I first started with miz3, I not only made more errors, I didn't understand what I was doing wrong. (Mizar, which seems to desire users to be ``less able to prove goals,'' has much better error messages than miz3.) So it would have been senseless for me to try to take big inference leaps when I started. Now I'm more confident, and take bigger inference leaps, and use timeout := 30;;. Freek didn't give miz3 enough credit above. Checking an unfinished proof with a large timeout isn't necessarily slow. Miz3 can often quickly spot that you don't have a proof and give you a #1 inference error. miz3 is only slow when you have a "by" justification that makes pretty good sense, and MESON works hard to prove that line. Some numbers may help. On a Linux box with a 2.4GHz processor and 4 GB RAM, my miz3 code http://www.math.northwestern.edu/~richter/RichterHOL-LightMiz3HilbertAxiomGeometry.tar.gz takes almost 5 minutes to run, and I have 41 6-digit MESON "solved at" numbers. Here's my highest: [...] 0..0..5..21..53..106..233..490..909..1725..3233..5819..10297..17188..26577..40416..67880..107813..185180..291684..445461..solved at 547963 [...] val EuclidProp11_THM : thm = |- !A B. ~(A = B) ==> (?F. Right (angle A B F)) I'm just proving that we can push a perpendicular off a line. I know which line of the proof earned the half-million MESON "solved at" number: F NOTIN l [notFl] by l_line, Distinct, I1, Collinear_DEF, Fexists, NOTIN; I actually have a bug in my code, and I'm surprised miz3 justified this at all! I'll discuss that in a separate post, but what I meant to write was F NOTIN l [notFl] by l_line, Cl, Collinear_DEF, -, NOTIN; and miz3 justifies that with a solved at number of 49, I think. But lets move on to how my HOL may be impeding MESON's efforts. I don't actually know which parts of my code are HOL. My first line of code is new_type("point",0);; which I think is HOL, and means take a set called point. In that sense, I'm doing HOL, right? I did that in my Tarski code too. But it gets worse: new_type_abbrev("point_set",`:point->bool`);; new_constant("Line",`:point_set->bool`);; So basically point_set = P(point), as sets are identified (or confused) with boolean functions, and I'm saying there is a boolean function Line defined on P(point), which is supposed to tell whether a set of points actually forms a line. That sounds like HOL. More crucial I think is my constant use of IN, defined in sets.ml as let IN = new_definition `!P:A->bool. !x. x IN P <=> P x`;; Everyone says that MESON can't do HOL, and I wonder if MESON can understand me when I use IN. My first definition is in fact about IN: let NOTIN = new_definition `!a:A l:A->bool. a NOTIN l <=> ~(a IN l)`;; -- Best, Bill ------------------------------------------------------------------------------ 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
