|
|
|
|
The gauge integral theory in HOL4
|
|
|
|
|
|
|
|
نویسنده
|
shi z. ,gu w. ,li x. ,guan y. ,ye s. ,zhang j. ,wei h.
|
|
منبع
|
journal of applied mathematics - 2013 - دوره : 2013 - شماره : 0
|
|
چکیده
|
The integral is one of the most important foundations for modeling dynamical systems. the gauge integral is a generalization of the riemann integral and the lebesgue integral and applies to a much wider class of functions. in this paper,we formalize the operational properties which contain the linearity,monotonicity,integration by parts,the cauchy-type integrability criterion,and other important theorems of the gauge integral in higher-order logic 4 (hol4) and then use them to verify an inverting integrator. the formalized theorem library has been accepted by the hol4 authority and will appear in hol4 kananaskis-9. © 2013 zhiping shi et al.
|
|
|
|
|
آدرس
|
beijing engineering research center of high reliable embedded system,capital normal university,beijing 100048,china,state key laboratory of computer architecture,institute of computing technology,chinese academy of sciences, China, beijing engineering research center of high reliable embedded system,capital normal university, China, beijing engineering research center of high reliable embedded system,capital normal university, China, beijing engineering research center of high reliable embedded system,capital normal university, China, college of information science and engineering,graduate university,chinese academy of sciences, China, college of information science and technology,beijing university of chemical technology, China, school of mechanical engineering and automation,beijing university of aeronautics and astronautics, China
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Authors
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|