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.
Michael On 17/03/2013, at 10:46, Vincent Aravantinos <[email protected]> wrote: > Hi list, > > I have two questions about the simplifier (in HOL Light and/or HOL4): > > 1. Is there a recent paper/documentation explaining the internals of the > simplifier? > (I know of the seminal paper by Larry Paulson, but there are quite > many improvements which have been achieved since then; > the notion of congruence, in particular, is essential in the current > simplifier - at least in HOL Light; > it seems the nowadays simplifier is the result of a lot of work by > Don Syme but a (quick) look at his publications did not yield any > satisfactory result) > > 2. Am I right that the simplifier can only achieve *invertible* > transformations of the goal? > i.e., if the simplifier turns a goal G1 into a goal G2, then G2 is > provable iff G1 is. > > Thanks, > V. > > -- > Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware > Verification Group > http://users.encs.concordia.ca/~vincent/ > > > ------------------------------------------------------------------------------ > 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 ------------------------------------------------------------------------------ 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
