The gauge integral theory in HOL4 (Q2375421): Difference between revisions
From MaRDI portal
Created claim: Wikidata QID (P12): Q59001913, #quickstatements; #temporary_batch_1712260040974 |
ReferenceBot (talk | contribs) Changed an Item |
||
Property / cites work | |||
Property / cites work: Theorem Proving in Higher Order Logics / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q2754041 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3497626 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: On the Formalization of the Lebesgue Integration Theory in HOL / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4231030 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4490681 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4307619 / rank | |||
Normal rank |
Latest revision as of 13:27, 6 July 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