Hi Bill, | Thanks, John! I'd be thrilled if you included my code in the HOL Light | distribution (miz3 dir sounds good)! I think it would improve my paper's | chance of being accepted.
OK, I'll be very happy to incorporate it whenever you regard it as final. Or if you prefer, I can put a preliminary version in now and it can be updated later. | I don't understand the technicalities, but may I make a suggestion? | No matter how powerful you make miz3, users can still put extra | details in their proofs. The purpose of extra details is good | pedagogy, so that another human can read the code and learn the proof. | I think my miz3 code is almost as readable as my paper, especially | with the fancy HOL4/Isabelle-style math fonts. If miz3 is really | powerful, then users are on the "honor system" as to whether they | really understand their own proofs, but math is already on the "honor | system", so it's fine. That's certainly a reasonable position. Of course, it also requires a reliable proof assistant (so that if it does prove a theorem you can be pretty sure it's right) and a good understanding of the underlying definitions or axioms (so that you are not deluded about what is being proved). Generally speaking, I'd say that "the automation is too powerful" is a problem we'd love to have! The situation probably arises more often in this domain of synthetic geometry because you really are trying to follow strict axiomatic reasoning using first-order logic, and in that case the computer can quite often beat the human (as in the Los puzzle). But in areas where the human is using some higher level of intuition and a mixture of domain-specific reasoning and logic, being beaten by the machine is a bit more unusual. | I wasn't clear about my time-table yesterday. I have 4 tasks left, in | increasing order of difficulty: | 1) finish formalizing the plane geometry parts of my 26 page paper (close to | done) | 2) port the new geometry rigor from my code to my paper (shouldn't take long, | and then I can write to Hartshorne) | 3) finish my miz3 users guide MizTips (I must understand Freek's syntax & | semantics lectures) | 4) understand HOL (I'm reading the HOL4 Logic manual) | | The last task sounds hard to me, and possibly I won't do a good job. The description of HOL in the Logic manual is based on a formal semantics inside set theory, developed by Andy Pitts. While this might be considered the ultimate reference, I'm not sure that it's necessarily the easiest place to start, even for a mathematician, if you want a satisfying intuitive understanding of the logic. My own (perhaps unhelpful) point of view is that if you think of types as nonempty sets, you can pretty much read statements at face value with the ordinary mathematical sense of "->" as function space etc. (I admit that polymorphic type variables slightly spoil this naive picture.) I don't think the correspondence between everyday informal mathematics and HOL is any more complicated than that between informal mathematics and ZF set theory. | So if you want to improve miz3 for my paper, you'll have time. | What I would most like you to look at my code and figure out why | MESON is working so hard. I have 16 MESON solved at numbers over | 200,000, but I don't think I ever ask miz3 to do anything as hard | as the Los Logic problem, which had a MESON solved at number about | 20,000. In general, algorithms like MESON for first-order proof search work by looking for proofs in certain standard forms. By imposing such restrictions, you sometimes need proofs that are longer than you might expect, but the advantage is that the search space to enumerate when trying to find proofs becomes smaller. There is a trade-off involved. The MESON algorithm is a form of model elimination, which is similar to another well-known algorithm called tableaux, except that (1) the formulas get put into clausal form initially, and (2) only tableau deductions with a certain "connection" between formulas are allowed. Among other things, this makes MESON relatively inefficient at using a logical equivalence |- !x. P[x] <=> Q[x] to "rewrite" P to Q inside another formula; the length of the required proof grows with the size of that formula, and replacement inside quantifiers may expand the search space further because you need to examine different instantiations. I think that accounts for your time-consuming B4' derivation, for example. John. ------------------------------------------------------------------------------ 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
