RODIN

Hello again guys,

Now I'm having troubles using fractional values, don't know how to resolve
things like 3/2 * K, because we're only able to use INT and NAT values,
what I resolved so far, is to replace the above formula by K + K/2, but as
you may notice this is rounding the numbers and loosing some precision, is
it possible to use real values or something similar?

Thanks in advance, best regards,

Rodolfo.

Re: [Rodin-b-sharp-user] Problem with fractional values From: Hoang, Thai Son <htson@in...> - 2013-01-13 22:43 Hi Rodolfo, I know that there are some push for having real numbers using the Theory plugin in Rodin, but I do not know how far that work goes. The best right now is to use context to define rational numbers, operations and axioms about these operations. Below can be a starting point CONTEXT Rational SETS RATIONAL CONSTANTS Frac /* Constructing a rational number from 2 integers */ Rmultiply /* Multiplication for rational numbers */ AXIOMS Frac : INT ** (INT \ {0}) --> RATIONAL Rmultiply : RATIONAL ** RATIONAL --> RATIONAL END It is not pretty, especially you will need to formulate a number of axioms about rational before you can do some interesting proofs. Cheers, Son On 13 Jan 2013, at 18:11, Rodolfo Campos <camposer@...>> wrote: Hello again guys, Now I'm having troubles using fractional values, don't know how to resolve things like 3/2 * K, because we're only able to use INT and NAT values, what I resolved so far, is to replace the above formula by K + K/2, but as you may notice this is rounding the numbers and loosing some precision, is it possible to use real values or something similar? Thanks in advance, best regards, Rodolfo. ------------------------------------------------------------------------------ Master Visual Studio, SharePoint, SQL, ASP.NET<http://ASP.NET>, C# 2012, HTML5, CSS, MVC, Windows 8 Apps, JavaScript and much more. Keep your skills current with LearnDevNow - 3,200 step-by-step video tutorials by Microsoft MVPs and experts. ON SALE this month only -- learn more at: http://p.sf.net/sfu/learnmore_123012_______________________________________________ Rodin-b-sharp-user mailing list Rodin-b-sharp-user@... https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user

Re: [Rodin-b-sharp-user] Problem with fractional values From: Rodolfo Campos <camposer@gm...> - 2013-01-14 10:20 Attachments: Message as HTML      Thank you very much Son, finally we solved the problem just isolating the variable, making something like: a < 3/2 b <=> 2a < 3b As easy as that, again, thank you very much for your help. Regards, Rodolfo. On Sun, Jan 13, 2013 at 11:42 PM, Hoang, Thai Son <htson@...> wrote: > Hi Rodolfo, > I know that there are some push for having real numbers using the Theory > plugin in Rodin, but I do not know how far that work goes. > The best right now is to use context to define rational numbers, > operations and axioms about these operations. Below can be a starting point > CONTEXT Rational > SETS RATIONAL > CONSTANTS > Frac /* Constructing a rational number from 2 integers */ > Rmultiply /* Multiplication for rational numbers */ > AXIOMS > Frac : INT ** (INT \ {0}) --> RATIONAL > Rmultiply : RATIONAL ** RATIONAL --> RATIONAL > END > > It is not pretty, especially you will need to formulate a number of > axioms about rational before you can do some interesting proofs. > Cheers, > Son > > > On 13 Jan 2013, at 18:11, Rodolfo Campos <camposer@...: > camposer@...>> > wrote: > > Hello again guys, > > Now I'm having troubles using fractional values, don't know how to resolve > things like 3/2 * K, because we're only able to use INT and NAT values, > what I resolved so far, is to replace the above formula by K + K/2, but as > you may notice this is rounding the numbers and loosing some precision, is > it possible to use real values or something similar? > > Thanks in advance, best regards, > > Rodolfo. > > ------------------------------------------------------------------------------ > Master Visual Studio, SharePoint, SQL, ASP.NET<http://ASP.NET>, C# 2012, > HTML5, CSS, > MVC, Windows 8 Apps, JavaScript and much more. Keep your skills current > with LearnDevNow - 3,200 step-by-step video tutorials by Microsoft > MVPs and experts. ON SALE this month only -- learn more at: > > http://p.sf.net/sfu/learnmore_123012_______________________________________________ > Rodin-b-sharp-user mailing list > Rodin-b-sharp-user@... > https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user > > > > ------------------------------------------------------------------------------ > Master Visual Studio, SharePoint, SQL, ASP.NET, C# 2012, HTML5, CSS, > MVC, Windows 8 Apps, JavaScript and much more. Keep your skills current > with LearnDevNow - 3,200 step-by-step video tutorials by Microsoft > MVPs and experts. ON SALE this month only -- learn more at: > http://p.sf.net/sfu/learnmore_123012 > _______________________________________________ > Rodin-b-sharp-user mailing list > Rodin-b-sharp-user@... > https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user >

2 messages have been excluded from this view by a project administrator.