<abstract xmlns="http://www.w3.org/1999/xhtml">

<p>In this paper, we introduce indefinite integrals [<xref ref-type="bibr" rid="j_forma-2023-0012_ref_008">8</xref>] (antiderivatives) and proof integration by substitution in the Mizar system [<xref ref-type="bibr" rid="j_forma-2023-0012_ref_002">2</xref>], [<xref ref-type="bibr" rid="j_forma-2023-0012_ref_003">3</xref>]. In our previous article [<xref ref-type="bibr" rid="j_forma-2023-0012_ref_015">15</xref>], we have introduced an indefinite-like integral, but it is inadequate because it must be an integral over the whole set of real numbers and in some sense it causes some duplication in the Mizar Mathematical Library [<xref ref-type="bibr" rid="j_forma-2023-0012_ref_013">13</xref>]. For this reason, to define the antiderivative for a function, we use the derivative of an arbitrary interval as defined recently in [<xref ref-type="bibr" rid="j_forma-2023-0012_ref_007">7</xref>]. Furthermore, antiderivatives are also used to modify the integration by substitution and integration by parts.</p>
<p>In the first section, we summarize the basic theorems on continuity and derivativity (for interesting survey of formalizations of real analysis in another proof-assistants like ACL2 [<xref ref-type="bibr" rid="j_forma-2023-0012_ref_012">12</xref>], Isabelle/HOL [<xref ref-type="bibr" rid="j_forma-2023-0012_ref_011">11</xref>], Coq [<xref ref-type="bibr" rid="j_forma-2023-0012_ref_004">4</xref>], see [<xref ref-type="bibr" rid="j_forma-2023-0012_ref_005">5</xref>]). In the second section, we generalize some theorems that were noticed during the formalization process. In the last section, we define the antiderivatives and formalize the integration by substitution and the integration by parts. We referred to [<xref ref-type="bibr" rid="j_forma-2023-0012_ref_001">1</xref>] and [<xref ref-type="bibr" rid="j_forma-2023-0012_ref_006">6</xref>] in our development.</p>
</abstract>

In this paper, we introduce indefinite integrals [8] (antiderivatives) and proof integration by substitution in the Mizar system [2], [3]. In our previous article [15], we have introduced an indefinite-like integral, but it is inadequate because it must be an integral over the whole set of real numbers and in some sense it causes some duplication in the Mizar Mathematical Library [13]. For this reason, to define the antiderivative for a function, we use the derivative of an arbitrary interval as defined recently in [7]. Furthermore, antiderivatives are also used to modify the integration by substitution and integration by parts.
In the first section, we summarize the basic theorems on continuity and derivativity (for interesting survey of formalizations of real analysis in another proof-assistants like ACL2 [12], Isabelle/HOL [11], Coq [4], see [5]). In the second section, we generalize some theorems that were noticed during the formalization process. In the last section, we define the antiderivatives and formalize the integration by substitution and the integration by parts. We referred to [1] and [6] in our development.

Antiderivatives and Integration

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 Public License.

{"article-title":"Antiderivatives and Integration"}

In this paper, we introduce indefinite integrals [8] (antiderivatives) and proof integration by substitution in the Mizar system [2], [3]. In our previous...

Antiderivatives and Integration

Data publikacji: 01 lis 2023

Zakres stron: 131 - 141

Przyjęty: 30 cze 2023

DOI: https://doi.org/10.2478/forma-2023-0012

Słowa kluczowe
antiderivative, integration by substitution

© 2023 Noboru Endou, published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 Public License.

Antiderivatives and Integration

Data publikacji: 01 lis 2023

Zakres stron: 131 - 141

Przyjęty: 30 cze 2023

DOI: https://doi.org/10.2478/forma-2023-0012

Słowa kluczoweantiderivative, integration by substitution

© 2023 Noboru Endou, published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 Public License.

Słowa kluczowe
antiderivative, integration by substitution