[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: formalizing integration



Sayan Mitra wrote:
> 
> Hello,
> 
> I am writing a theory in PVS and I need to write simple expressions
> involving integration, say eg.
> 
> v(t)  = \Int a(t) dt
> 
> And then prove lemmas like :
> 
> If a(t) =  0  over a range of t then v(t) remains constant .
> 
> I have not found a theory which formalizes integration. Can someone tell
> me a way of doing this ? Thank you very much,
> 
> regrads
> Sayan
> 

There are PVS analysis libraries that define continuity,
limits, and differentiation. You could use them 
for developing a theory of integration, but that probably
requires a lot of work. 

The libraries include results such as 

  null_derivative : PROPOSITION
        constant(g) IFF (FORALL x : deriv(g, x) = 0)

This kind of proposition may be all that you need.
The basic library is available at

http://www.sdl.sri.com/users/bruno/pvs-stuff.html

or at the NASA Langley library web site:

http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/pvslib.html

The NASA web site also has extensions of this library 
and related theories (e.g., trigonometric functions).
There are also extensions developed by Hanne Gottliebsen
at St Andrews:

http://www-theory.dcs.st-and-ac.uk/~hago/research.html

If you really need integration, you may want to look at a paper
by John Harrison and Laurent Thery, that describes something
similar using HOL:

@ARTICLE{harrison-cas,
        author          = "John Harrison and Laurent Th{\'e}ry",
        title           = "A Skeptic's Approach to Combining {HOL} 
                           and {M}aple",
        journal         = "Journal of Automated Reasoning",
        volume          = 21,
        pages           = "279--294",
        year            = 1998}
 


Bruno Dutertre
---
Bruno Dutertre                             | bruno@sdl.sri.com
SDL, SRI International                     | fax: 650 859-2844
333 Ravenswood Avenue, Menlo Park CA 94025 | tel: 650 859-2717