Screenshot instructions:
Windows
Mac
Red Hat Linux
Ubuntu
Click URL instructions:
Rightclick on ad, choose "Copy Link", then paste here →
(This may not be possible with some types of ads)
From: Matthias Schmalz <Matthias.S<chmalz@in...>  20090424 08:38:22

BEGIN PGP SIGNED MESSAGE Hash: SHA1 Ken, I am not aware of any documentation, and I agree with you that such documentation would be very useful. I realize that not so many people know what is going on inside the provers. So I will write a wikipage about it. Cheers, Matthias Ken Robinson schrieb: > Matthias, > > On 24/04/2009, at 01:47 AM, Matthias Schmalz wrote: > >> Unfortunately, the problem of finding a smallest set of required >> hypotheses is at least as hard as finding a proof  undecidable. >> Currently, there are three ways to select hypotheses: P0 or newPP >> restricted selects the hypotheses you see. >> P1 or newPP lassoo applies one lassoo operation and passes the >> result to >> the prover. The lassoo operation adds any hypothesis that has a common >> free symbol with some hypothesis that you could see before. >> PP and newPP select all hypotheses. >> My experience is, if you have a larger model, then only the first >> way  >> selecting the required hypotheses manually  works well. >> >> It would be interesting to think about some mechanisms that select the >> hypothesis in a smarter way than now. >> >> I hope you have a better prover experience in the future, > > Yes, thanks, and I do realise that there is no solution to finding a > proof. Unfortunately, for me at least, the provers and the prover > interface in Rodin is a black box. It's not clear what each set of > provers does differently one learns by trial and error and it's > certainly not clear "what happens" when you "run" a prover, and by > that I mean how the hypotheses are handled, etc. > > Is there any documentation on any of this? > > Cheers, > > Ken > >  > Crystal Reports  New Free Runtime and 30 Day Trial > Check out the new simplified licensign option that enables unlimited > royaltyfree distribution of the report engine for externally facing > server and web deployment. > http://p.sf.net/sfu/businessobjects > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser BEGIN PGP SIGNATURE Version: GnuPG v1.4.6 (GNU/Linux) Comment: Using GnuPG with Mozilla  http://enigmail.mozdev.org iD8DBQFJ8XpiczhznXSdWggRAvtkAJ0aFC+RWKT7LGVekX/7b7efyflSuwCgoLuT EZsDFHlTbFQuSFbr3njXlUU= =BgbE END PGP SIGNATURE 
From: Ken Robinson <kenr@cs...>  20090423 13:50:21

I can't find anything about this in the language document, but I am getting the impression that subset may be restricted to finite sets? I the following PO products +> NAT <: PRODUCT +> NAT where products is a fine subset of PRODUCT. It seems to me that the subset relation is reasonable, but I cannot get the Rodin provers to discharge it. If I replace NAT by a finite set then it does discharge, hence my conclusion above. Is that conclusion correct? I would not be asking this question if products was not finite: clearly there are elements in the rhs set that are not in the lhs set, so subset seems reasonable? Cheers, Ken 
From: Thai Son Hoang <htson@in...>  20090423 13:59:50

Dear Ken, Ken Robinson wrote: > I can't find anything about this in the language document, but I am > getting the impression that subset may be restricted to finite sets? > > I the following PO > > products +> NAT <: PRODUCT +> NAT > > where products is a fine subset of PRODUCT. > > It seems to me that the subset relation is reasonable, but I cannot > get the Rodin provers to discharge it. > > If I replace NAT by a finite set then it does discharge, hence my > conclusion above. > > Is that conclusion correct? > > I would not be asking this question if products was not finite: > clearly there are elements in the rhs set that are not in the lhs set, > so subset seems reasonable? > I have the following context, CONTEXT ctx SETS PRODUCT CONSTANTS products AXIOMS axm1 : products ⊆ PRODUCT THEOREMS thm1 : products ⇸ ℕ ⊆ PRODUCT ⇸ ℕ END The theorem is proved interactively by clicking on the "<:" follows by ML. I do not know the actual consequence of this, but it seems like automatically expanding "<:" is not the strategy of existing provers. Cheers, Son P/S: I guess there is no problem with finiteness at all (even products is not finite). 
From: Ken Robinson <kenr@cs...>  20090423 14:33:53

Dear Son, Thanks for that, but ... On 23/04/2009, at 23:58 PM, Thai Son Hoang wrote: > Ken Robinson wrote: >> I can't find anything about this in the language document, but I am >> getting the impression that subset may be restricted to finite sets? >> >> I the following PO >> >> products +> NAT <: PRODUCT +> NAT >> >> where products is a fine subset of PRODUCT. >> >> It seems to me that the subset relation is reasonable, but I cannot >> get the Rodin provers to discharge it. >> >> If I replace NAT by a finite set then it does discharge, hence my >> conclusion above. >> >> Is that conclusion correct? >> >> I would not be asking this question if products was not finite: >> clearly there are elements in the rhs set that are not in the lhs >> set, >> so subset seems reasonable? >> > > I have the following context, > CONTEXT > ctx > SETS > PRODUCT > CONSTANTS > products > AXIOMS > axm1 : products ⊆ PRODUCT > THEOREMS > thm1 : products ⇸ ℕ ⊆ PRODUCT ⇸ ℕ > END > > The theorem is proved interactively by clicking on the "<:" follows > by ML. Not when I do it. It doesn't discharge. But nevertheless you have removed any doubt about finiteness. The only difference between your example and mine is that products is a variable in mine, and in mine PRODUCT is declared as finite. More interesting is that in my case, even replacing NAT by a finite set, the lemma is not discharged by ml, it requires one of the npp provers. Must be some strange problem with my Rodin, or something. :( Cheers, Ken 
From: Matthias Schmalz <Matthias.S<chmalz@in...>  20090423 15:01:14

BEGIN PGP SIGNED MESSAGE Hash: SHA1 Ken, all available hypotheses are passed to ML. In your case, ML probably gets distracted by irrelevant hypotheses. In Son's case there are no irrelevant hypotheses. It is hard to predict what newPP and PP can discharge. I would proceed as follows: 1. remove all hypotheses, but "products <: PRODUCT" 2. try newPP (restricted) and P0. 3. If that fails start to unfold the goal and try the automatic provers again and again. 4. If some subgoals cannot be discharged, then please send them to us. Best regards, Matthias Ken Robinson schrieb: > Dear Son, > > Thanks for that, but ... > > On 23/04/2009, at 23:58 PM, Thai Son Hoang wrote: > >> Ken Robinson wrote: >>> I can't find anything about this in the language document, but I am >>> getting the impression that subset may be restricted to finite sets? >>> >>> I the following PO >>> >>> products +> NAT <: PRODUCT +> NAT >>> >>> where products is a fine subset of PRODUCT. >>> >>> It seems to me that the subset relation is reasonable, but I cannot >>> get the Rodin provers to discharge it. >>> >>> If I replace NAT by a finite set then it does discharge, hence my >>> conclusion above. >>> >>> Is that conclusion correct? >>> >>> I would not be asking this question if products was not finite: >>> clearly there are elements in the rhs set that are not in the lhs >>> set, >>> so subset seems reasonable? >>> >> I have the following context, >> CONTEXT >> ctx >> SETS >> PRODUCT >> CONSTANTS >> products >> AXIOMS >> axm1 : products ⊆ PRODUCT >> THEOREMS >> thm1 : products ⇸ ℕ ⊆ PRODUCT ⇸ ℕ >> END >> >> The theorem is proved interactively by clicking on the "<:" follows >> by ML. > > Not when I do it. It doesn't discharge. > > But nevertheless you have removed any doubt about finiteness. The > only difference between your example and mine is that products is a > variable in mine, and in mine PRODUCT is declared as finite. > > More interesting is that in my case, even replacing NAT by a finite > set, the lemma is not discharged by ml, it requires one of the npp > provers. > > Must be some strange problem with my Rodin, or something. :( > > Cheers, > > Ken > >  > Stay on top of everything new and different, both inside and > around Java (TM) technology  register by April 22, and save > $200 on the JavaOne (SM) conference, June 25, 2009, San Francisco. > 300 plus technical and handson sessions. Register today. > Use priority code J9JMT32. http://p.sf.net/sfu/p > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser BEGIN PGP SIGNATURE Version: GnuPG v1.4.6 (GNU/Linux) Comment: Using GnuPG with Mozilla  http://enigmail.mozdev.org iD8DBQFJ8IKnczhznXSdWggRAhGMAJ98T/rnkvCxnZifY6yyzvD09zaYvACgjilk APhR5OdHdw1EqsnB2XImb+k= =TpII END PGP SIGNATURE 
From: Ken Robinson <kenr@cs...>  20090423 15:28:59

Matthias, On 24/04/2009, at 01:00 AM, Matthias Schmalz wrote: > BEGIN PGP SIGNED MESSAGE > > all available hypotheses are passed to ML. In your case, ML probably > gets distracted by irrelevant hypotheses. In Son's case there are no > irrelevant hypotheses. > It is hard to predict what newPP and PP can discharge. I would proceed > as follows: > 1. remove all hypotheses, but "products <: PRODUCT" > 2. try newPP (restricted) and P0. > 3. If that fails start to unfold the goal and try the automatic > provers > again and again. > 4. If some subgoals cannot be discharged, then please send them to us. Thank you very much. That was a very useful lesson. I never realised the problem of having too many hypotheses. Once I removed all hypotheses except the critical one it discharged instantly. I've always worked on the principle of "the more hypotheses, the better", and often that does seem to be the case. I realise that you only need some critical subset, but I guess the easy thing to do is to drag in as many as possible. Hmmm. It's interesting that given a large set somehow the provers don't finally pick on the right hypotheses to use. There must be some limiting process involved? Cheers, Ken > > > Best regards, > > Matthias > > Ken Robinson schrieb: >> Dear Son, >> >> Thanks for that, but ... >> >> On 23/04/2009, at 23:58 PM, Thai Son Hoang wrote: >> >>> Ken Robinson wrote: >>>> I can't find anything about this in the language document, but I am >>>> getting the impression that subset may be restricted to finite >>>> sets? >>>> >>>> I the following PO >>>> >>>> products +> NAT <: PRODUCT +> NAT >>>> >>>> where products is a fine subset of PRODUCT. >>>> >>>> It seems to me that the subset relation is reasonable, but I cannot >>>> get the Rodin provers to discharge it. >>>> >>>> If I replace NAT by a finite set then it does discharge, hence my >>>> conclusion above. >>>> >>>> Is that conclusion correct? >>>> >>>> I would not be asking this question if products was not finite: >>>> clearly there are elements in the rhs set that are not in the lhs >>>> set, >>>> so subset seems reasonable? >>>> >>> I have the following context, >>> CONTEXT >>> ctx >>> SETS >>> PRODUCT >>> CONSTANTS >>> products >>> AXIOMS >>> axm1 : products ⊆ PRODUCT >>> THEOREMS >>> thm1 : products ⇸ ℕ ⊆ PRODUCT ⇸ ℕ >>> END >>> >>> The theorem is proved interactively by clicking on the "<:" follows >>> by ML. >> >> Not when I do it. It doesn't discharge. >> >> But nevertheless you have removed any doubt about finiteness. The >> only difference between your example and mine is that products is a >> variable in mine, and in mine PRODUCT is declared as finite. >> >> More interesting is that in my case, even replacing NAT by a finite >> set, the lemma is not discharged by ml, it requires one of the npp >> provers. >> >> Must be some strange problem with my Rodin, or something. :( >> >> Cheers, >> >> Ken >> >>  >> Stay on top of everything new and different, both inside and >> around Java (TM) technology  register by April 22, and save >> $200 on the JavaOne (SM) conference, June 25, 2009, San Francisco. >> 300 plus technical and handson sessions. Register today. >> Use priority code J9JMT32. http://p.sf.net/sfu/p >> _______________________________________________ >> Rodinbsharpuser mailing list >> Rodinbsharpuser@... >> https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser > BEGIN PGP SIGNATURE > Version: GnuPG v1.4.6 (GNU/Linux) > Comment: Using GnuPG with Mozilla  http://enigmail.mozdev.org > > iD8DBQFJ8IKnczhznXSdWggRAhGMAJ98T/rnkvCxnZifY6yyzvD09zaYvACgjilk > APhR5OdHdw1EqsnB2XImb+k= > =TpII > END PGP SIGNATURE > >  > Stay on top of everything new and different, both inside and > around Java (TM) technology  register by April 22, and save > $200 on the JavaOne (SM) conference, June 25, 2009, San Francisco. > 300 plus technical and handson sessions. Register today. > Use priority code J9JMT32. http://p.sf.net/sfu/p > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser 
From: Matthias Schmalz <Matthias.S<chmalz@in...>  20090423 15:48:20

BEGIN PGP SIGNED MESSAGE Hash: SHA1 Ken, Ken Robinson schrieb: > Matthias, > > On 24/04/2009, at 01:00 AM, Matthias Schmalz wrote: > > all available hypotheses are passed to ML. In your case, ML probably > gets distracted by irrelevant hypotheses. In Son's case there are no > irrelevant hypotheses. > It is hard to predict what newPP and PP can discharge. I would proceed > as follows: > 1. remove all hypotheses, but "products <: PRODUCT" > 2. try newPP (restricted) and P0. > 3. If that fails start to unfold the goal and try the automatic > provers > again and again. > 4. If some subgoals cannot be discharged, then please send them to us. > >> Thank you very much. That was a very useful lesson. I never realised >> the problem of having too many hypotheses. Once I removed all >> hypotheses except the critical one it discharged instantly. > >> I've always worked on the principle of "the more hypotheses, the >> better", and often that does seem to be the case. I realise that you >> only need some critical subset, but I guess the easy thing to do is to >> drag in as many as possible. Hmmm. > >> It's interesting that given a large set somehow the provers don't >> finally pick on the right hypotheses to use. There must be some >> limiting process involved? Unfortunately, the problem of finding a smallest set of required hypotheses is at least as hard as finding a proof  undecidable. Currently, there are three ways to select hypotheses: P0 or newPP restricted selects the hypotheses you see. P1 or newPP lassoo applies one lassoo operation and passes the result to the prover. The lassoo operation adds any hypothesis that has a common free symbol with some hypothesis that you could see before. PP and newPP select all hypotheses. My experience is, if you have a larger model, then only the first way  selecting the required hypotheses manually  works well. It would be interesting to think about some mechanisms that select the hypothesis in a smarter way than now. I hope you have a better prover experience in the future, Matthias BEGIN PGP SIGNATURE Version: GnuPG v1.4.6 (GNU/Linux) Comment: Using GnuPG with Mozilla  http://enigmail.mozdev.org iD8DBQFJ8I2nczhznXSdWggRAl5zAJ9B36hC56HvYW6sVPzh0c/XbudrsQCfWhRS 8xh/7Vi3o29chd+wgCfoJ2c= =EN9G END PGP SIGNATURE 
From: Ken Robinson <kenr@cs...>  20090424 05:14:40

Matthias, On 24/04/2009, at 01:47 AM, Matthias Schmalz wrote: > Unfortunately, the problem of finding a smallest set of required > hypotheses is at least as hard as finding a proof  undecidable. > Currently, there are three ways to select hypotheses: P0 or newPP > restricted selects the hypotheses you see. > P1 or newPP lassoo applies one lassoo operation and passes the > result to > the prover. The lassoo operation adds any hypothesis that has a common > free symbol with some hypothesis that you could see before. > PP and newPP select all hypotheses. > My experience is, if you have a larger model, then only the first > way  > selecting the required hypotheses manually  works well. > > It would be interesting to think about some mechanisms that select the > hypothesis in a smarter way than now. > > I hope you have a better prover experience in the future, Yes, thanks, and I do realise that there is no solution to finding a proof. Unfortunately, for me at least, the provers and the prover interface in Rodin is a black box. It's not clear what each set of provers does differently one learns by trial and error and it's certainly not clear "what happens" when you "run" a prover, and by that I mean how the hypotheses are handled, etc. Is there any documentation on any of this? Cheers, Ken 
From: Matthias Schmalz <Matthias.S<chmalz@in...>  20090424 08:38:22

BEGIN PGP SIGNED MESSAGE Hash: SHA1 Ken, I am not aware of any documentation, and I agree with you that such documentation would be very useful. I realize that not so many people know what is going on inside the provers. So I will write a wikipage about it. Cheers, Matthias Ken Robinson schrieb: > Matthias, > > On 24/04/2009, at 01:47 AM, Matthias Schmalz wrote: > >> Unfortunately, the problem of finding a smallest set of required >> hypotheses is at least as hard as finding a proof  undecidable. >> Currently, there are three ways to select hypotheses: P0 or newPP >> restricted selects the hypotheses you see. >> P1 or newPP lassoo applies one lassoo operation and passes the >> result to >> the prover. The lassoo operation adds any hypothesis that has a common >> free symbol with some hypothesis that you could see before. >> PP and newPP select all hypotheses. >> My experience is, if you have a larger model, then only the first >> way  >> selecting the required hypotheses manually  works well. >> >> It would be interesting to think about some mechanisms that select the >> hypothesis in a smarter way than now. >> >> I hope you have a better prover experience in the future, > > Yes, thanks, and I do realise that there is no solution to finding a > proof. Unfortunately, for me at least, the provers and the prover > interface in Rodin is a black box. It's not clear what each set of > provers does differently one learns by trial and error and it's > certainly not clear "what happens" when you "run" a prover, and by > that I mean how the hypotheses are handled, etc. > > Is there any documentation on any of this? > > Cheers, > > Ken > >  > Crystal Reports  New Free Runtime and 30 Day Trial > Check out the new simplified licensign option that enables unlimited > royaltyfree distribution of the report engine for externally facing > server and web deployment. > http://p.sf.net/sfu/businessobjects > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser BEGIN PGP SIGNATURE Version: GnuPG v1.4.6 (GNU/Linux) Comment: Using GnuPG with Mozilla  http://enigmail.mozdev.org iD8DBQFJ8XpiczhznXSdWggRAvtkAJ0aFC+RWKT7LGVekX/7b7efyflSuwCgoLuT EZsDFHlTbFQuSFbr3njXlUU= =BgbE END PGP SIGNATURE 
From: Ken Robinson <kenr@cs...>  20090424 08:50:36

Matthias, On 24/04/2009, at 18:37 PM, Matthias Schmalz wrote: > I am not aware of any documentation, and I agree with you that such > documentation would be very useful. > I realize that not so many people know what is going on inside the > provers. > So I will write a wikipage about it. That would be great. Thanks, Ken > Ken Robinson schrieb: >> Matthias, >> >> On 24/04/2009, at 01:47 AM, Matthias Schmalz wrote: >> >>> Unfortunately, the problem of finding a smallest set of required >>> hypotheses is at least as hard as finding a proof  undecidable. >>> Currently, there are three ways to select hypotheses: P0 or newPP >>> restricted selects the hypotheses you see. >>> P1 or newPP lassoo applies one lassoo operation and passes the >>> result to >>> the prover. The lassoo operation adds any hypothesis that has a >>> common >>> free symbol with some hypothesis that you could see before. >>> PP and newPP select all hypotheses. >>> My experience is, if you have a larger model, then only the first >>> way  >>> selecting the required hypotheses manually  works well. >>> >>> It would be interesting to think about some mechanisms that select >>> the >>> hypothesis in a smarter way than now. >>> >>> I hope you have a better prover experience in the future, >> >> Yes, thanks, and I do realise that there is no solution to finding a >> proof. Unfortunately, for me at least, the provers and the prover >> interface in Rodin is a black box. It's not clear what each set of >> provers does differently one learns by trial and error and it's >> certainly not clear "what happens" when you "run" a prover, and by >> that I mean how the hypotheses are handled, etc. >> >> Is there any documentation on any of this? >> >> Cheers, >> >> Ken >> >>  >> Crystal Reports  New Free Runtime and 30 Day Trial >> Check out the new simplified licensign option that enables unlimited >> royaltyfree distribution of the report engine for externally >> facing >> server and web deployment. >> http://p.sf.net/sfu/businessobjects >> _______________________________________________ >> Rodinbsharpuser mailing list >> Rodinbsharpuser@... >> https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser > BEGIN PGP SIGNATURE > Version: GnuPG v1.4.6 (GNU/Linux) > Comment: Using GnuPG with Mozilla  http://enigmail.mozdev.org > > iD8DBQFJ8XpiczhznXSdWggRAvtkAJ0aFC+RWKT7LGVekX/7b7efyflSuwCgoLuT > EZsDFHlTbFQuSFbr3njXlUU= > =BgbE > END PGP SIGNATURE > >  > Crystal Reports  New Free Runtime and 30 Day Trial > Check out the new simplified licensign option that enables unlimited > royaltyfree distribution of the report engine for externally > facing > server and web deployment. > http://p.sf.net/sfu/businessobjects > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser 
From: Jonathan S. Ostroff <jonathan@yo...>  20090424 15:06:15

It would be great to have more information about the provers and prover strategy. Thanks for producing such a nice tool. Jonathan Original Message From: Matthias Schmalz [mailto:Matthias.Schmalz@...] Sent: Friday, April 24, 2009 4:38 AM To: User Rodin Bsharp Subject: Re: [Rodinbsharpuser] Subset and finiteness BEGIN PGP SIGNED MESSAGE Hash: SHA1 Ken, I am not aware of any documentation, and I agree with you that such documentation would be very useful. I realize that not so many people know what is going on inside the provers. So I will write a wikipage about it. Cheers, Matthias Ken Robinson schrieb: > Matthias, > > On 24/04/2009, at 01:47 AM, Matthias Schmalz wrote: > >> Unfortunately, the problem of finding a smallest set of required >> hypotheses is at least as hard as finding a proof  undecidable. >> Currently, there are three ways to select hypotheses: P0 or newPP >> restricted selects the hypotheses you see. >> P1 or newPP lassoo applies one lassoo operation and passes the >> result to >> the prover. The lassoo operation adds any hypothesis that has a common >> free symbol with some hypothesis that you could see before. >> PP and newPP select all hypotheses. >> My experience is, if you have a larger model, then only the first >> way  >> selecting the required hypotheses manually  works well. >> >> It would be interesting to think about some mechanisms that select the >> hypothesis in a smarter way than now. >> >> I hope you have a better prover experience in the future, > > Yes, thanks, and I do realise that there is no solution to finding a > proof. Unfortunately, for me at least, the provers and the prover > interface in Rodin is a black box. It's not clear what each set of > provers does differently one learns by trial and error and it's > certainly not clear "what happens" when you "run" a prover, and by > that I mean how the hypotheses are handled, etc. > > Is there any documentation on any of this? > > Cheers, > > Ken > >   > Crystal Reports  New Free Runtime and 30 Day Trial > Check out the new simplified licensign option that enables unlimited > royaltyfree distribution of the report engine for externally facing > server and web deployment. > http://p.sf.net/sfu/businessobjects > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser BEGIN PGP SIGNATURE Version: GnuPG v1.4.6 (GNU/Linux) Comment: Using GnuPG with Mozilla  http://enigmail.mozdev.org iD8DBQFJ8XpiczhznXSdWggRAvtkAJ0aFC+RWKT7LGVekX/7b7efyflSuwCgoLuT EZsDFHlTbFQuSFbr3njXlUU= =BgbE END PGP SIGNATURE   Crystal Reports  New Free Runtime and 30 Day Trial Check out the new simplified licensign option that enables unlimited royaltyfree distribution of the report engine for externally facing server and web deployment. http://p.sf.net/sfu/businessobjects _______________________________________________ Rodinbsharpuser mailing list Rodinbsharpuser@... https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser 
Sign up for the SourceForge newsletter:
No, thanks