On 08/08/12 11:21, Bill Richter wrote: > Thanks, Michael! HOL Light does not have your EVAL, but maybe it has > something similar. EVAL is indeed the sort of thing that Colin Rowat and I > were looking for. I did read a bit about rewriting, and I see that it's in > the EVAL ballpark, but it sounds like you have to be pretty good at HOL Light > to use it. Any tip?
The first point of entry is probably REWRITE_CONV [my_definition_thm]. That is a function of type term -> thm, so will enable you to "test" terms' behaviours. The more definitions you put into the list passed to REWRITE_CONV, the more you will get out. > Can you jump into the discussion Michael and I were having about > whether miz3 is intentionally weakened? Michael seems to think yes, > I think no, but I wonder what effect the MESON depth limit of 50 > has, or the fact that MESON is just FOL and not HOL. My claim is based on my believing that miz3 imposes a time limit, and that there is a depth limit in MESON more generally (perhaps I'm wrong about these). Both of these things will stop miz3's "by" from proving things that it might otherwise. Hence it is "intentionally weakened". That weakening then helps to limit the size of the inference jumps you can make. I do not think this is a bad thing. The fact that MESON is FOL and not HOL will probably make it unable to prove theorems like EVERY (\x. P (f x y)) [a; b; c] where EVERY is the (higher-order) function that checks that all elements of a list satisfy the predicate that is passed as EVERY's first argument. Michael ------------------------------------------------------------------------------ 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
