The gauge integral theory in HOL4 (Q2375421)

From MaRDI portal
scientific article
In more languages
Configure
Language Label Description Also known as
English
The gauge integral theory in HOL4
scientific article

    Statements

    The gauge integral theory in HOL4 (English)
    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.
    gauge integral
    Cauchy-type integrability criterion
    higher-order logic
    HOL4 Kananaskis-9

    Identifiers