Journal of Applied Mathematics
Volume 2013 (2013), Article ID 160875, 7 pages
http://dx.doi.org/10.1155/2013/160875
Research Article

The Gauge Integral Theory in HOL4

Zhiping Shi,1,2 Weiqing Gu,1 Xiaojuan Li,1 Yong Guan,1 Shiwei Ye,3 Jie Zhang,4 and Hongxing Wei5

1Beijing Engineering Research Center of High Reliable Embedded System, Capital Normal University, Beijing 100048, China
2State Key Laboratory of Computer Architecture, Institute of Computing Technology, Chinese Academy of Sciences, Beijing 100190, China
3College of Information Science and Engineering, Graduate University of Chinese Academy of Sciences, Beijing 100049, China
4College of Information Science and Technology, Beijing University of Chemical Technology, Beijing 100029, China
5School of Mechanical Engineering and Automation, Beijing University of Aeronautics and Astronautics, Beijing 100191, China

Received 6 February 2013; Accepted 27 February 2013

Academic Editor: Xiaoyu Song

Copyright © 2013 Zhiping Shi et al. This is an open access article distributed under the Creative Commons Attribution License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.

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.