The Gauge Integral Theory in HOL4
Joint Authors
Li, Xiaojuan
Wei, Hongxing
Ye, Shiwei
Zhang, Jie
Guan, Yong
Gu, Weiqing
Shi, Zhiping
Source
Journal of Applied Mathematics
Issue
Vol. 2013, Issue 2013 (31 Dec. 2013), pp.1-7, 7 p.
Publisher
Hindawi Publishing Corporation
Publication Date
2013-05-02
Country of Publication
Egypt
No. of Pages
7
Main Subjects
Abstract EN
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.
American Psychological Association (APA)
Shi, Zhiping& Gu, Weiqing& Li, Xiaojuan& Guan, Yong& Ye, Shiwei& Zhang, Jie…[et al.]. 2013. The Gauge Integral Theory in HOL4. Journal of Applied Mathematics،Vol. 2013, no. 2013, pp.1-7.
https://search.emarefa.net/detail/BIM-450700
Modern Language Association (MLA)
Shi, Zhiping…[et al.]. The Gauge Integral Theory in HOL4. Journal of Applied Mathematics No. 2013 (2013), pp.1-7.
https://search.emarefa.net/detail/BIM-450700
American Medical Association (AMA)
Shi, Zhiping& Gu, Weiqing& Li, Xiaojuan& Guan, Yong& Ye, Shiwei& Zhang, Jie…[et al.]. The Gauge Integral Theory in HOL4. Journal of Applied Mathematics. 2013. Vol. 2013, no. 2013, pp.1-7.
https://search.emarefa.net/detail/BIM-450700
Data Type
Journal Articles
Language
English
Notes
Includes bibliographical references
Record ID
BIM-450700
