[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


or at the NASA Langley library web site:


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:


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:

        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