Great, I'll have a look, thank you all!
--
Vincent Aravantinos
PostDoctoral Fellow, Concordia University, Hardware Verification Group
http://users.encs.concordia.ca/~vincent
Le 2013-03-16 à 23:16, Konrad Slind <[email protected]> a écrit :
> 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
