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
