> > 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