The Gauge Integral Theory in HOL4
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 line...
Saved in:
| Main Authors: | , , , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Wiley
2013-01-01
|
| Series: | Journal of Applied Mathematics |
| Online Access: | http://dx.doi.org/10.1155/2013/160875 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1832554160744038400 |
|---|---|
| author | Zhiping Shi Weiqing Gu Xiaojuan Li Yong Guan Shiwei Ye Jie Zhang Hongxing Wei |
| author_facet | Zhiping Shi Weiqing Gu Xiaojuan Li Yong Guan Shiwei Ye Jie Zhang Hongxing Wei |
| author_sort | Zhiping Shi |
| collection | DOAJ |
| description | 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. |
| format | Article |
| id | doaj-art-7d8832f8a0394cfc918a52931a96b236 |
| institution | Kabale University |
| issn | 1110-757X 1687-0042 |
| language | English |
| publishDate | 2013-01-01 |
| publisher | Wiley |
| record_format | Article |
| series | Journal of Applied Mathematics |
| spelling | doaj-art-7d8832f8a0394cfc918a52931a96b2362025-02-03T05:52:17ZengWileyJournal of Applied Mathematics1110-757X1687-00422013-01-01201310.1155/2013/160875160875The Gauge Integral Theory in HOL4Zhiping Shi0Weiqing Gu1Xiaojuan Li2Yong Guan3Shiwei Ye4Jie Zhang5Hongxing Wei6Beijing Engineering Research Center of High Reliable Embedded System, Capital Normal University, Beijing 100048, ChinaBeijing Engineering Research Center of High Reliable Embedded System, Capital Normal University, Beijing 100048, ChinaBeijing Engineering Research Center of High Reliable Embedded System, Capital Normal University, Beijing 100048, ChinaBeijing Engineering Research Center of High Reliable Embedded System, Capital Normal University, Beijing 100048, ChinaCollege of Information Science and Engineering, Graduate University of Chinese Academy of Sciences, Beijing 100049, ChinaCollege of Information Science and Technology, Beijing University of Chemical Technology, Beijing 100029, ChinaSchool of Mechanical Engineering and Automation, Beijing University of Aeronautics and Astronautics, Beijing 100191, ChinaThe 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.http://dx.doi.org/10.1155/2013/160875 |
| spellingShingle | Zhiping Shi Weiqing Gu Xiaojuan Li Yong Guan Shiwei Ye Jie Zhang Hongxing Wei The Gauge Integral Theory in HOL4 Journal of Applied Mathematics |
| title | The Gauge Integral Theory in HOL4 |
| title_full | The Gauge Integral Theory in HOL4 |
| title_fullStr | The Gauge Integral Theory in HOL4 |
| title_full_unstemmed | The Gauge Integral Theory in HOL4 |
| title_short | The Gauge Integral Theory in HOL4 |
| title_sort | gauge integral theory in hol4 |
| url | http://dx.doi.org/10.1155/2013/160875 |
| work_keys_str_mv | AT zhipingshi thegaugeintegraltheoryinhol4 AT weiqinggu thegaugeintegraltheoryinhol4 AT xiaojuanli thegaugeintegraltheoryinhol4 AT yongguan thegaugeintegraltheoryinhol4 AT shiweiye thegaugeintegraltheoryinhol4 AT jiezhang thegaugeintegraltheoryinhol4 AT hongxingwei thegaugeintegraltheoryinhol4 AT zhipingshi gaugeintegraltheoryinhol4 AT weiqinggu gaugeintegraltheoryinhol4 AT xiaojuanli gaugeintegraltheoryinhol4 AT yongguan gaugeintegraltheoryinhol4 AT shiweiye gaugeintegraltheoryinhol4 AT jiezhang gaugeintegraltheoryinhol4 AT hongxingwei gaugeintegraltheoryinhol4 |