On Sat, May 5, 2012 at 11:24 AM, "Mark" <[email protected]> wrote:
> Makarius wrote:
> > I've looked at holzero-0.4.1 before and just today at
> > holzero-0.5.4. (I am still hoping to see a really
> > convincing independent proof checker for the HOL family
> > of systems.)
>
> In what sense is HOL Zero not a convincincly independent implementation of
> the HOL logic? Its development was sponsored by no-one other than myself.
> Its core system (inference kernel + parser/printer + core theory) was all
> genuinely written from scratch - it took about 5 iterations to get variable
> instantiation right!! Its architecture involves the innovation of an inner
> (or "language") kernel, inside the inference kernel. Its parser, printer
> and concrete syntax involve numerous innovations; they are, for the first
> time in a HOL system, compatible, well-behaved and input-complete
> (according
> to definitions in Freek's Pollack Inconsistency paper). The specification
> (but not implementation) of its 800 ML interface objects (equivalents of
> 'assoc', 'frees', 'INST', etc) was largely derived from the pre-existing
> HOL
> systems, but this was done by careful consideration of each system's
> behaviour in turn.
>
For the record, OpenTheory (http://www.gilith.com/research/opentheory/) is
also an independent implementation of HOL, and may be treated as a separate
proof checker. It wasn't written with the same soundness goals as HOL Zero,
though; I would still recommend HOL Zero for checking when soundness is a
major concern.
------------------------------------------------------------------------------
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
