Hi Vincent:
Michael has done a thorough job of documenting the simplifier: see
Section 5.5.4 of the Description.
Konrad.
On Sat, Mar 16, 2013 at 7:38 PM, 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.
>
> 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
>
------------------------------------------------------------------------------
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
