Hi Bill, > 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.
The reasoning is that speed implies easy refactoring, and that facilitates optimization of the library. Making the library quickly processable is also useful for all kinds of research over it and processing of various kinds. The speed can really make a lot of difference in how humans interact with computers. I think Linus Torvalds once said that the raw speed of his "git" version control system significantly changed the way he uses version control. With massive parallelization (64 CPUs on one machine) I can now process the whole MML below 10 minutes, and this kind of near-real-time interactivity makes experimental research in large-scale formal math quite a bit of fun. But I think the original intention behind the "weakness" was to capture the right level of reasoning that would be "obvious" to humans, i.e., not too strong to puzzle the readers and not too weak to drown them in detail. This motivation is probably still quite strong, although occasionally I hear even some Mizar people say heresies like "Who reads the proofs?" :-). > And so presumably if you make improvements in library calls, then Mizar would > want to become stronger. Is that right? The "library calls" are (in Mizar) theorems, definitions, and typing automations. If they become stronger and more mutually compatible, then formalization is indeed easier. Particularly the Coq people have been recently doing a lot of research in how to make formal math as re-usable as possible. It is a fairly interesting and nontrivial topic. > One thing I can't understand is how Mizar weakens itself in the first place. One of the best descriptions is actually John's code for "holby" in HOL Light :-). Also Freek has compiled a description here: http://www.cs.ru.nl/~freek/mizar/by.ps.gz . The motivation is in the "obvious inference" papers by Davis and Rudnicki that I already mentioned. > 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, There are really many proof search procedures (and ways how to limit them and combine them). > and you seemed to say it yourself: [Mizar's] own "MESON" - "by". That was a crude analogy, sorry for the confusion. Both "MESON" and "by" are the respective workhorses in HOL Light and Mizar, but they do different things. Josef ------------------------------------------------------------------------------ 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
