Pełnotekstowe zasoby PLDML oraz innych baz dziedzinowych są już dostępne w nowej Bibliotece Nauki.
Zapraszamy na https://bibliotekanauki.pl
Preferencje help
Polish version English version Język
Widoczny [Schowaj] Abstrakt
Liczba wyników

Znaleziono wyników: 7

Liczba wyników na stronie
first rewind previous Strona / 1 next fast forward last

Wyniki wyszukiwania

help Sortuj według:

help Ogranicz wyniki do:
first rewind previous Strona / 1 next fast forward last
1
Content available remote

A Note on the Seven Bridges of Königsberg Problem

100%
Naumowicz A.
Formalized Mathematics
|
2014
|
tom 22
|
nr 2
177-178
EN
In this paper we account for the formalization of the seven bridges of Königsberg puzzle. The problem originally posed and solved by Euler in 1735 is historically notable for having laid the foundations of graph theory, cf. [7]. Our formalization utilizes a simple set-theoretical graph representation with four distinct sets for the graph’s vertices and another seven sets that represent the edges (bridges). The work appends the article by Nakamura and Rudnicki [10] by introducing the classic example of a graph that does not contain an Eulerian path. This theorem is item #54 from the “Formalizing 100 Theorems” list maintained by Freek Wiedijk at http://www.cs.ru.nl/F.Wiedijk/100/.
2
Content available remote

On the Representation of Natural Numbers in Positional Numeral Systems1

100%
Naumowicz A.
Formalized Mathematics
|
2006
|
tom 14
|
nr 4
221-223
EN
In this paper we show that every natural number can be uniquely represented as a base-b numeral. The formalization is based on the proof presented in [11]. We also prove selected divisibility criteria in the base-10 numeral system.
3
Content available remote

Niven’s Theorem

64%
Korniłowicz A., Naumowicz A.
Formalized Mathematics
|
2016
|
tom 24
|
nr 4
301-308
EN
This article formalizes the proof of Niven’s theorem [12] which states that if x/π and sin(x) are both rational, then the sine takes values 0, ±1/2, and ±1. The main part of the formalization follows the informal proof presented at Pr∞fWiki (https://proofwiki.org/wiki/Niven’s_Theorem#Source_of_Name). For this proof, we have also formalized the rational and integral root theorems setting constraints on solutions of polynomial equations with integer coefficients [8, 9].
4
Content available remote

More on Divisibility Criteria for Selected Primes

64%
Naumowicz A., Piliszek R.
Formalized Mathematics
|
2013
|
tom 21
|
nr 2
87-94
EN
This paper is a continuation of [19], where the divisibility criteria for initial prime numbers based on their representation in the decimal system were formalized. In the current paper we consider all primes up to 101 to demonstrate the method presented in [7].
5
Content available remote

All Liouville Numbers are Transcendental

51%
Korniłowicz A., Naumowicz A., Grabowski A.
Formalized Mathematics
|
2017
|
tom 25
|
nr 1
49-54
EN
In this Mizar article, we complete the formalization of one of the items from Abad and Abad’s challenge list of “Top 100 Theorems” about Liouville numbers and the existence of transcendental numbers. It is item #18 from the “Formalizing 100 Theorems” list maintained by Freek Wiedijk at http://www.cs.ru.nl/F.Wiedijk/100/. Liouville numbers were introduced by Joseph Liouville in 1844 [15] as an example of an object which can be approximated “quite closely” by a sequence of rational numbers. A real number x is a Liouville number iff for every positive integer n, there exist integers p and q such that q > 1 and [...] It is easy to show that all Liouville numbers are irrational. The definition and basic notions are contained in [10], [1], and [12]. Liouvile constant, which is defined formally in [12], is the first explicit transcendental (not algebraic) number, another notable examples are e and π [5], [11], and [4]. Algebraic numbers were formalized with the help of the Mizar system [13] very recently, by Yasushige Watase in [23] and now we expand these techniques into the area of not only pure algebraic domains (as fields, rings and formal polynomials), but also for more settheoretic fields. Finally we show that all Liouville numbers are transcendental, based on Liouville’s theorem on Diophantine approximation.
6
Content available remote

Partial Differentiation, Differentiation and Continuity onn-Dimensional Real Normed Linear Spaces

51%
Inoué T., Naumowicz A., Endou N., Shidama Y.
Formalized Mathematics
|
2011
|
tom 19
|
nr 2
65-68
EN
In this article, we aim to prove the characterization of differentiation by means of partial differentiation for vector-valued functions on n-dimensional real normed linear spaces (refer to [15] and [16]).
7
Content available remote

Partial Differentiation of Vector-Valued Functions onn-Dimensional Real Normed Linear Spaces

51%
Inoué T., Naumowicz A., Endou N., Shidama Y.
Formalized Mathematics
|
2011
|
tom 19
|
nr 1
1-9
EN
In this article, we define and develop partial differentiation of vector-valued functions on n-dimensional real normed linear spaces (refer to [19] and [20]).
first rewind previous Strona / 1 next fast forward last
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.