Bill or Michael in particular, one question:
On Thu, Aug 30, 2012 at 7:39 PM, Bill Richter <[email protected]
> wrote:
> 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.
>
To what document is Bill referring here as Michael's "Logic manual"?
Thanks in advance,
Cris
>
> 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
>
------------------------------------------------------------------------------
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
