The gauge integral theory in HOL4

DOI10.1155/2013/160875zbMath1268.65033OpenAlexW2066086825WikidataQ59001913 ScholiaQ59001913MaRDI QIDQ2375421

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

Publication date: 14 June 2013

Published in: Journal of Applied Mathematics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1155/2013/160875

zbMATH Keywords

higher-order logicgauge integralCauchy-type integrability criterionHOL4 Kananaskis-9

Mathematics Subject Classification ID

Integration of real functions of several variables: length, area, volume (26B15) Numerical integration (65D30) Packaged methods for numerical algorithms (65Y15)

Related Items (2)

Formalization of function matrix theory in HOL ⋮ Verified interactive computation of definite integrals

Uses Software

• Isabelle/HOL
• HOL

Cites Work

• Theorem Proving in Higher Order Logics
• On the Formalization of the Lebesgue Integration Theory in HOL
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: The gauge integral theory in HOL4