The Gauge Integral Theory in HOL4

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

Journal of Applied Mathematics, 2013, vol. 2013, issue 1

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.

Date: 2013
References: Add references at CitEc
Citations:

Downloads: (external link)
https://doi.org/10.1155/2013/160875

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:wly:jnljam:v:2013:y:2013:i:1:n:160875

Access Statistics for this article

More articles in Journal of Applied Mathematics from John Wiley & Sons
Bibliographic data for series maintained by Wiley Content Delivery ().