REPOZYTORIUM UNIWERSYTETU
W BIAŁYMSTOKU
UwB

  1. Repozytorium Uniwersytetu w Białymstoku
  2. Czasopisma naukowe / Journals
  3. Formalized Mathematics
  4. Formalized Mathematics, 2025, Volume 33, Issue 1

Szukanie zaawansowane
  • Zespoły i Kolekcje


  • Zaloguj się
  • Zarejestruj się
  • Mój RUB
  • FAQ
  • Polityka
  • Regulamin
  • DOI
  • Instrukcja
  • Aspekty prawne
  • Open Access
  • Archiwum


  • Kontakt
  • O Dspace
  • Strona Biblioteki
  • Strona Uczelni



    • Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji: http://hdl.handle.net/11320/19654
    Pełny rekord metadanych
    Pole DCWartośćJęzyk
    dc.contributor.authorWatase, Yasushige-
    dc.date.accessioned2026-01-26T11:46:58Z-
    dc.date.available2026-01-26T11:46:58Z-
    dc.date.issued2025-
    dc.identifier.citationFormalized Mathematics, Volume 33, Issue 1, Pages 85-94pl
    dc.identifier.issn1426-2630-
    dc.identifier.urihttp://hdl.handle.net/11320/19654-
    dc.description.abstractIn this article, we develop the proof of the so-called Wallis formula using the Mizar formalism. The purpose of this formalization is to complete the proof of Stirling’s formula using elementary techniques of calculus; however, the formal encoding of the Wallis-type integral is also included.pl
    dc.language.isoenpl
    dc.publisherUniversity of Białystokpl
    dc.rightsAttribution-ShareAlike 4.0 International (CC BY-SA 4.0)pl
    dc.rights.urihttps://creativecommons.org/licenses/by-sa/4.0/pl
    dc.subjectWallis integralpl
    dc.subjectStirling formulapl
    dc.titleFormalization of Wallis Infinite Product Formula for π and the Wallis Integralpl
    dc.typeArticlepl
    dc.rights.holder2025 The Author(s)pl
    dc.rights.holderCC BY-SA 4.0 licensepl
    dc.identifier.doi10.2478/forma-2025-0007-
    dc.description.AffiliationFaculty of Data Science, University of Rissho, Magechi Kumagaya, Japanpl
    dc.description.referencesYves Bertot. A short presentation of Coq. In Otmane Aıt Mohamed, C´esar A. Munoz, and Sofiene Tahar, editors, Theorem Proving in Higher Order Logics (TPHOLs 2008), volume 5170 of LNCS, pages 12–16. Springer, 2008. doi:10.1007/978-3-540-71067-7_3.pl
    dc.description.referencesRichard Courant and Fritz John. Introduction to Calculus and Analysis I. John Wiley and Sons Inc., New York, 1st edition, 1965.pl
    dc.description.referencesManuel Eberl. Stirling’s formula. Archive of Formal Proofs, September 2016. https: //isa-afp.org/entries/Stirling_Formula.html, Formal proof development.pl
    dc.description.referencesAdam Grabowski, Artur Korniłowicz, and Adam Naumowicz. Four decades of Mizar. Journal of Automated Reasoning, 55(3):191–198, 2015. doi:10.1007/s10817-015-9345-1.pl
    dc.description.referencesJohn Harrison. Stirling’s approximation. 2010. Available online at https://github.com/jrh13/hol-light/blob/master/100/stirling.ml.pl
    dc.description.referencesNobushige Kurokawa. Modern Trigonometric Function Theory. Iwanami Shoten, Publishers (Tokyo), 1st edition, 2013. In Japanese.pl
    dc.description.referencesNorman D. Megill and David A. Wheeler. Metamath: A Computer Language for Mathematical Proofs. Lulu Press, Morrisville, North Carolina, 2019. http://us.metamath.org/downloads/metamath.pdf.pl
    dc.description.referencesLeonardo de Moura and Sebastian Ullrich. The Lean 4 theorem prover and programming language. In Automated Deduction – CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings, pages 625–635, Berlin, Heidelberg, 2021. Springer-Verlag. doi:10.1007/978-3-030-79876-5_37.pl
    dc.description.referencesKarol Pąk. Leibniz series for π. Formalized Mathematics, 24(4):275–280, 2016. doi:10.1515/forma-2016-0023.pl
    dc.description.referencesChristoph Schwarzweller. The binomial theorem for algebraic structures. Formalized Mathematics, 9(3):559–564, 2001.pl
    dc.description.referencesYasunari Shidama, Noboru Endou, and Katsumi Wasaki. Riemann indefinite integral of functions of real variable. Formalized Mathematics, 15(2):59–63, 2007.doi:10.2478/v10037-007-0007-6.pl
    dc.description.referencesYasushige Watase. Formal proof of transcendence of the number e. Part II. Formalized Mathematics, 32(1):121–131, 2024. doi:10.2478/forma-2024-0009.pl
    dc.description.referencesFreek Wiedijk. Formalizing 100 theorems. Available online at http://www.cs.ru.nl/~freek/100/.pl
    dc.description.referencesYuguang Yang and Yasunari Shidama. Trigonometric functions and existence of circle ratio. Formalized Mathematics, 7(2):255–263, 1998.pl
    dc.identifier.eissn1898-9934-
    dc.description.volume33pl
    dc.description.issue1pl
    dc.description.firstpage85pl
    dc.description.lastpage94pl
    dc.identifier.citation2Formalized Mathematicspl
    Występuje w kolekcji(ach):Formalized Mathematics, 2025, Volume 33, Issue 1

    Pliki w tej pozycji:
    Plik Opis RozmiarFormat 
    Formalization_of_Wallis_Infinite_Product_Formula_for_π_and_the_Wallis_Integral.pdf282,62 kBAdobe PDFOtwórz
    Pokaż uproszczony widok rekordu Zobacz statystyki


    Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL Creative Commons