>
> 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 setting
full automation is not achievable, either on the grounds of
undecidability of the theory you are working in, or very high
computational complexity. So maybe you are saying: "there
should be an algorithm, or heuristic, that efficiently proves all
statements that are obvious (to me)". That was the
approach of the early pioneers in automated proof, but resolution
theorem proving swept that notion aside, and I am not sure on what
scientific basis that could be revived. (Since "obvious" is a nebulous
conceptual blob of an idea.)
Or are you just saying that you wish
MESON proved more things more quickly? (In which case, why not
use the prover9 interface, which I think HOL-Light provides. Maybe you'll
get lucky!)
> The description of HOL in the Logic manual is based on a formal
> semantics inside set theory, developed by Andy Pitts.
>
> I see Andy wrote a paper with your advisor The HOL Logic and System but I
> can't find a pdf for it.
http://www.cl.cam.ac.uk/ftp/hvg/papers/HOLPaper.ps.gz
The first part, at least, provides something like what you seem to be
looking for.
Konrad.
------------------------------------------------------------------------------
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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
