Thanks for the HOL lesson, Michael, and clarifying about theorem-proving! Can you give me some advice on how to read your 45 page Logic manual? I need to understand why
x : point [means] "x is an element of the set point" (the reading we can derive using the semantics) Your Logic manual looks perfectly rigorous but it has real exposition problems for mathematicians like me. Once I understand it, I'll try to make some suggestions on how to improve the exposition. Perhaps it's written for people who already know everything that I'm struggling with. Who wouldn't rather be doing deep stuff? I'd be happy to work on software verification, even it's "tedious in the computer, and unimaginably tedious with pen and paper". Right now I don't have the skill, and my next step is to learn procedural proofs. Let's try to settle this miz3 biz, and my first step is: Josef, my conjecture was wrong, and I regret my disparaging remarks about Mizar monkeying around with timeout numbers. Piotr Rudnickii's article Obvious Inferences explains very interesting and sensible FOL, and his Herbrand stuff is discussed in John's book. But my larger points (or Michael's) still hold, as Piotr explains: PR> In defining the class of obvious inferences there is a danger of PR> introducing a discrepancy between the user's sense of an obvious PR> inference and what the proof-checker is able to accept. Right, no FOL can't define what humans mean by obvious, so if Mizar's Herbrand obvious inference stuff actually captures our meaning of obvious, we're hitting Michael's sweet spot, and thinking Mizar always captures obvious our meaning of obvious is an illusion. PR> Firstly, the goal is to force students to write proofs in detail, PR> thus not all correct inferences have to be accepted. I am against this goal, and John has several times posted it is not his goal, most strongly today: JH> Generally speaking, I'd say that "the automation is too powerful" JH> is a problem we'd love [miz3] to have! Michael, the issue with Freek and miz3 is whether Freek intended to force students to write proofs in detail by setting timeout = 1 in miz3. I believe (not sure) that he said that was not his intention. What we know for sure is that Freek 1) often explains that one should set the timeout higher, even to -1 (no timeout) 2) explained the reason for timeout = 1: to limit user frustration when miz3 is trying very hard to prove something that's obviously wrong. By setting timeout = 1, you get immediate feedback. What I said, and Freek didn't necessarily agree with, is that this immediate feedback is particularly important for new users, and I feel quite comfortable with timeout = 50. I think Freek still often uses timeout = 1 for immediate feedback. All this makes for a good comparison between Freek and Heineken, which installs beer bottle tops to prevent stores and consumers from spilling the beer, not to force users to drink less. And really, why do we care? That's easy! I want a smart HOL guy like you to think about how we can make miz3 (holby, actually) more powerful. I'm having a bad interaction, I hazily conjecture, between the FOL that MESON is good at and the set theory in my paper. For that, you must understand that intentional weakness isn't a miz3 goal, for then you efforts would be wasted. -- 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
