The Gauge Integral Theory in HOL4. (2nd May 2013)

• Record Type: Journal Article
• Authors: Shi, Zhiping; Gu, Weiqing; Li, Xiaojuan; Guan, Yong; Ye, Shiwei; Zhang, Jie; Wei, Hongxing
• Other Names: Song Xiaoyu Academic Editor.
• Is Part Of: Journal of applied mathematics. Volume 2013(2013)
• Publication Date: 2013-05-02
• Subjects: Mathematics -- Periodicals; 519.05
• DOI: 10.1155/2013/160875
• Languages: English
• ISSNs: 1110-757X

Abstract

Abstract : 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.