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

*To*: Sayan Mitra <mitras@csa.iisc.ernet.in>*Subject*: Re: formalizing integration*From*: Bruno Dutertre <bruno@sdl.sri.com>*Date*: Mon, 16 Apr 2001 10:09:21 -0700*CC*: pvs-help@csl.sri.com*References*: <Pine.LNX.4.10.10104132200460.2934-100000@ruby.csa.iisc.ernet.in>*Sender*: pvs-help-owner@csl.sri.com

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

**References**:**formalizing integration***From:*Sayan Mitra <mitras@csa.iisc.ernet.in>

- Prev by Date:
**formalizing integration** - Next by Date:
**Defining a finite (super)type.** - Prev by thread:
**formalizing integration** - Next by thread:
**Record-type equality bug??** - Index(es):