Bill or Michael in particular, one question:
On Thu, Aug 30, 2012 at 7:39 PM, Bill Richter 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 [mea
>
>Generally speaking, I'd say that "the automation is too powerful"
>is a problem we'd love [miz3] to have!
>
> Great! Right now it's not powerful enough for me.
Bill, I'm struggling to understand your point of view. Of course,
more automation is a good thing, but presumably in your sett
Michael, that's extremely helpful, I need to read the part about
[p 17] The meaning of HOL terms in such a model will now be described.
and terms means constants as well as abstractions. I should be able to decode
your simple picture from the general description there. Page 19 more
formidab
On 31/08/12 12:39, Bill Richter 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
>> der
Thanks, John! Please take my code whenever you like. I'm done coding, and
I'll regard my tar.gz file to be final after I fold my miz3 improvement back
into my paper and finish my Miz3Tips file, which only requires me to understand
Freek's syntax, and he just made a contribution to that, explai
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 ma
Hi Bill,
Thanks a lot for the detailed discussion of how the angle sum theorem
is typically proved in standard texts, and how the formalization goes.
It's been chastening to me to discover how hard it can be to formalize
what I thought was easy during my schooldays!
| let ANGLES_ADD_BETWEEN = pr
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 preli
On 30/08/2012, at 17:58, Bill Richter wrote:
> Michael, I detect in your previous post a disturbing definition of
> theorem-proving:
> [Bill] is mathematically sophisticated but a novice as far as
> theorem-proving is concerned.
> I think I'm quite good at theorem-proving (I have 11 pape
Michael, I detect in your previous post a disturbing definition of
theorem-proving:
[Bill] is mathematically sophisticated but a novice as far as
theorem-proving is concerned.
I think I'm quite good at theorem-proving (I have 11 papers published in Math
journals). I'm a novice at forma
10 matches
Mail list logo
