The gauge integral theory in HOL4 (Q2375421): Difference between revisions
From MaRDI portal
Set OpenAlex properties. |
Created claim: Wikidata QID (P12): Q59001913, #quickstatements; #temporary_batch_1712260040974 |
||
Property / Wikidata QID | |||
Property / Wikidata QID: Q59001913 / rank | |||
Normal rank |
Revision as of 21:54, 4 April 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | The gauge integral theory in HOL4 |
scientific article |
Statements
The gauge integral theory in HOL4 (English)
0 references
14 June 2013
0 references
Summary: 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.
0 references
gauge integral
0 references
Cauchy-type integrability criterion
0 references
higher-order logic
0 references
HOL4 Kananaskis-9
0 references