Hi Bill,
> ... My main problem is that I don't understand HOL, so I don't know what
> theorems HOL Light is proving for me. The HOL4 Logic manual looks like
> a very respectable CS document, but I haven't been able to read it yet,
and
> it's not a HOL Light document.
And it's not a particularly light HOL document either! I agree we are
missing a neat self-contained informal explanation of the HOL language and
logic. I'm trying to think of a good paper to point you to. Maybe Tom
Hale's AMS paper from 2008. Alternatively, chapters 3 & 4 of my incomplete
HOL Zero manual (bundled with the HOL Zero system) explain everything, but
then this is for HOL Zero and not for HOL Light, although it may still be
helpful for your purposes.
> With my Tarski code, I would be happy to
> say (though I don't quite understand it) that HOL Light was verifying my
FOL
> proofs using Tarski's geometry axioms. But there's real HOL in my
Hilbert
> code funneled through sets.ml. Of course I know what results I meant to
> prove, and my results use sets as mathematicians customarily use sets. I
> figure that's the result that HOL Light proved for me, but I'm missing the
> translation.
I'm not sure exactly what you mean when you say "translation".
Specifically, a translation from what to what? The "from" or the "to" could
conceivably be:
HOL Light term quotation syntax
HOL Light primitive term syntax
HOL Light miz3 proof scripts
HOL Light inference rules
conventional mathematical notation
some formal mathematical logic that is not HOL
Mark.
------------------------------------------------------------------------------
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
