Re: [isabelle] Interval Type



Your best bet is to contact the folks doing interval arithmetic research: reliable_computing at interval.louisiana.edu and interval at listserv.utep.edu.

To the point, there has been recent discussions on the mis- representation of intervals by Mathematica. The problems become very complex, really quickly, if you're doing symbolic mathematics on intervals.
--
steve
steve at cs.clemson.edu



On Jun 28, 2006, at 8:35 PM, Jeremy Dawson wrote:

Francisco Jose Chaves Alonso wrote:
Hello
I want to implement the interval arithmetic for use in the proof of expressions
like:
     x \<in> [0,1] ==> x * (1 – x) \<in> [0,1]
The interval [a,b] is the set of real numbers  { x | a <= x <= b}.
Based on the work of Daumas et al. on PVS,
http://research.nianet.org/~munoz/Papers/arith-17.pdf,
the idea is to show that x*(1 – x) is in the interval X*(1 – X) where X is the interval [0,1], and then show that X*(1 – X) \<subseteq> [0,1]. The operations
on intervals are defined such that
X at Y = { x at y | x \<in> X /\ y \<in> Y }, @ \<in> {+,-,*,/}
To model the intervals I have at least the following possibilities:
datatype interval = Interval real * real
record interval =
           lb:: real
           ub:: real
types interval:: real * real
which could be a good choice for Isabelle? Other possibilities or suggestions?
Thanks
Francisco
-- Francisco José Cháves (ENS-LIP)
mailto: Francisco.Jose.Chaves.Alonso at ens-lyon.fr
http://perso.ens-lyon.fr/francisco.jose.chaves.alonso
ENS de Lyon - 46, allee d'Italie - 69364 Lyon Cedex 07 - FRANCE
Phone: (+33) 4 72 72 84 36

Francisco,

I did some work on intervals of real numbers some years ago.
The work was based on some existing literature, and involved sets of intervals (more complicated than single intervals!) which could be either open or closed at either endpoint.

It was written up in

Jeremy E. Dawson & Rajeev Goré, Machine-checking the Timed Interval Calculus, 15th Australian Joint Conference on Artificial Intelligence (AI'02), LNCS 2557, 95-106,

see http://users.rsise.anu.edu.au/~jeremy/pubs/tic/

Software files in Isabelle are at

http://users.rsise.anu.edu.au/~jeremy/isabelle/tic/

Jeremy










This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.