REPOZYTORIUM UNIWERSYTETU
W BIAŁYMSTOKU

Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji: `http://hdl.handle.net/11320/15444`
 Tytuł: Antiderivatives and Integration Autorzy: Endou, Noboru Słowa kluczowe: antiderivativeintegration by substitution Data wydania: 2023 Data dodania: 9-lis-2023 Wydawca: DeGruyter Open Źródło: Formalized Mathematics, Volume 31, Issue 1, Pages 131-141 Abstrakt: 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. Afiliacja: National Institute of Technology, Gifu College, 2236-2 Kamimakuwa, Motosu, Gifu, Japan URI: http://hdl.handle.net/11320/15444 DOI: 10.2478/forma-2023-0012 ISSN: 1426-2630 e-ISSN: 1898-9934 metadata.dc.identifier.orcid: 0000-0002-5922-2332 Typ Dokumentu: Article metadata.dc.rights.uri: https://creativecommons.org/licenses/by-sa/3.0/ Właściciel praw: © 2023 The Author(s)CC BY-SA 3.0 license Występuje w kolekcji(ach): Formalized Mathematics, 2023, Volume 31, Issue 1

Pliki w tej pozycji:
Plik Opis RozmiarFormat