I believe the answer to your second question is yes, both in the sense that
invertibility is a design goal and that I think it's true. (I'm not very
confident :))
However, I don't know about any documentation... it would be great to find
or write some. This paper may be relevant:
http://dblp.uni-trier.de/rec/bibtex/journals/jar/Norrish09
On Sat, Mar 16, 2013 at 11:46 PM, 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
