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

formalizing integration


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,



Sayan Mitra

Dept. Computer Science and Automation, 
Indian Institute of Science
Bangalore 560012
Tel : 309-2625 (r) 309-2912 (l)
URL: www2.csa.iisc.ernet.in/~mitras