On 17 Mar 2013, at 00:38, Michael Norrish <[email protected]> wrote:
> The HOL4 Description manual has a section on the simplifier. And yes, it > should preserve the probability of goals because at the top level, it is only > capable of replacing equals with equals. > I am not convinced. I often set up a goal that I rate as highly probable, but when I rewrite it to 1 = 2 or suchlike, the probability takes a dive. That replacing equals with equals preserves provability, I believe. :-) Regards, Rob. ------------------------------------------------------------------------------ Everyone hates slow websites. So do we. Make your web apps faster with AppDynamics Download AppDynamics Lite for free today: http://p.sf.net/sfu/appdyn_d2d_mar _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
