Journal of Applied Mathematics (Jan 2013)

The Gauge Integral Theory in HOL4

  • Zhiping Shi,
  • Weiqing Gu,
  • Xiaojuan Li,
  • Yong Guan,
  • Shiwei Ye,
  • Jie Zhang,
  • Hongxing Wei

DOI
https://doi.org/10.1155/2013/160875
Journal volume & issue
Vol. 2013

Abstract

Read online

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.