rss_2.0Formalized Mathematics FeedSciendo RSS Feed for Formalized Mathematicshttps://sciendo.com/journal/FORMAhttps://www.sciendo.comFormalized Mathematics 's Coverhttps://sciendo-parsed-data-feed.s3.eu-central-1.amazonaws.com/62c9e63dca8f8703463c7662/cover-image.jpg?X-Amz-Algorithm=AWS4-HMAC-SHA256&X-Amz-Date=20221205T065604Z&X-Amz-SignedHeaders=host&X-Amz-Expires=604800&X-Amz-Credential=AKIA6AP2G7AKP25APDM2%2F20221205%2Feu-central-1%2Fs3%2Faws4_request&X-Amz-Signature=10eedff6ef91da7e7472861dacdb90a6148f572d450e4684cf1b9d245214c21a200300Improper Integral. Part Ihttps://sciendo.com/article/10.2478/forma-2021-0019<abstract>
<title style='display:none'>Summary</title>
<p>In this article, we deal with Riemann’s improper integral [1], using the Mizar system [2], [3]. Improper integrals with finite values are discussed in [5] by Yamazaki et al., but in general, improper integrals do not assume that they are finite. Therefore, we have formalized general improper integrals that does not limit the integral value to a finite value. In addition, each theorem in [5] assumes that the domain of integrand includes a closed interval, but since the improper integral should be discusses based on the half-open interval, we also corrected it.</p>
</abstract>Finite Dimensional Real Normed Spaces are Proper Metric Spaceshttps://sciendo.com/article/10.2478/forma-2021-0017<abstract>
<title style='display:none'>Summary</title>
<p>In this article, we formalize in Mizar [1], [2] the topological properties of finite-dimensional real normed spaces. In the first section, we formalize the Bolzano-Weierstrass theorem, which states that a bounded sequence of points in an n-dimensional Euclidean space has a certain subsequence that converges to a point. As a corollary, it is also shown the equivalence between a subset of an n-dimensional Euclidean space being compact and being closed and bounded.</p>
<p>In the next section, we formalize the definitions of L1-norm (Manhattan Norm) and maximum norm and show their topological equivalence in n-dimensional Euclidean spaces and finite-dimensional real linear spaces. In the last section, we formalize the linear isometries and their topological properties. Namely, it is shown that a linear isometry between real normed spaces preserves properties such as continuity, the convergence of a sequence, openness, closeness, and compactness of subsets. Finally, it is shown that finite-dimensional real normed spaces are proper metric spaces. We referred to [5], [9], and [7] in the formalization.</p>
</abstract>The 3-Fold Product Space of Real Normed Spaces and its Propertieshttps://sciendo.com/article/10.2478/forma-2021-0022<abstract>
<title style='display:none'>Summary</title>
<p>In this article, we formalize in Mizar [1], [2] the 3-fold product space of real normed spaces for usefulness in application fields such as engineering, although the formalization of the 2-fold product space of real normed spaces has been stored in the Mizar Mathematical Library [3].</p>
<p>First, we prove some theorems about the 3-variable function and 3-fold Cartesian product for preparation. Then we formalize the definition of 3-fold product space of real linear spaces. Finally, we formulate the definition of 3-fold product space of real normed spaces. We referred to [7] and [6] in the formalization.</p>
</abstract>Improper Integral. Part IIhttps://sciendo.com/article/10.2478/forma-2021-0024<abstract>
<title style='display:none'>Summary</title>
<p>In this article, using the Mizar system [2], [3], we deal with Riemann’s improper integral on infinite interval [1]. As with [4], we referred to [6], which discusses improper integrals of finite values.</p>
</abstract>About Graph Sumshttps://sciendo.com/article/10.2478/forma-2021-0023<abstract>
<title style='display:none'>Summary</title>
<p>In this article the sum (or disjoint union) of graphs is formalized in the Mizar system [4], [1], based on the formalization of graphs in [9].</p>
</abstract>Relationship between the Riemann and Lebesgue Integralshttps://sciendo.com/article/10.2478/forma-2021-0018<abstract>
<title style='display:none'>Summary</title>
<p>The goal of this article is to clarify the relationship between Riemann and Lebesgue integrals. In previous article [5], we constructed a one-dimensional Lebesgue measure. The one-dimensional Lebesgue measure provides a measure of any intervals, which can be used to prove the well-known relationship [6] between the Riemann and Lebesgue integrals [1]. We also proved the relationship between the integral of a given measure and that of its complete measure. As the result of this work, the Lebesgue integral of a bounded real valued function in the Mizar system [2], [3] can be calculated by the Riemann integral.</p>
</abstract>Prime Representing Polynomialhttps://sciendo.com/article/10.2478/forma-2021-0020<abstract>
<title style='display:none'>Summary</title>
<p>The main purpose of formalization is to prove that the set of prime numbers is diophantine, i.e., is representable by a polynomial formula. We formalize this problem, using the Mizar system [1], [2], in two independent ways, proving the existence of a polynomial without formulating it explicitly as well as with its indication.</p>
<p>First, we reuse nearly all the techniques invented to prove the MRDP-theorem [11]. Applying a trick with Mizar schemes that go beyond first-order logic we give a short sophisticated proof for the existence of such a polynomial but without formulating it explicitly. Then we formulate the polynomial proposed in [6] that has 26 variables in the Mizar language as follows (<italic>w</italic>·<italic>z</italic>+<italic>h</italic>+<italic>j</italic>−<italic>q</italic>)<sup>2</sup>+((<italic>g</italic>·<italic>k</italic>+<italic>g</italic>+<italic>k</italic>)·(<italic>h</italic>+<italic>j</italic>)+<italic>h</italic>−<italic>z</italic>)<sup>2</sup>+(2 · <italic>k</italic><sup>3</sup>·(2·<italic>k</italic>+2)·(<italic>n</italic> + 1)<sup>2</sup>+1−<italic>f</italic><sup>2</sup>)<sup>2</sup>+ (<italic>p</italic> + <italic>q</italic> + <italic>z</italic> + 2 · <italic>n</italic> − <italic>e</italic>)<sup>2</sup> + (<italic>e</italic><sup>3</sup> · (<italic>e</italic> + 2) · (<italic>a</italic> + 1)<sup>2</sup> + 1 − <italic>o</italic><sup>2</sup>)<sup>2</sup> + (<italic>x</italic><sup>2</sup> − (<italic>a</italic><sup>2</sup> −′ 1) · <italic>y</italic><sup>2</sup> − 1)<sup>2</sup> + (16 · (<italic>a</italic><sup>2</sup> − 1) · <italic>r</italic><sup>2</sup> · <italic>y</italic><sup>2</sup> · <italic>y</italic><sup>2</sup> + 1 − <italic>u</italic><sup>2</sup>)<sup>2</sup> + (((<italic>a</italic> + <italic>u</italic><sup>2</sup> · (<italic>u</italic><sup>2</sup> − <italic>a</italic>))<sup>2</sup> − 1) · (<italic>n</italic> + 4 · <italic>d</italic> · <italic>y</italic>)<sup>2</sup> + 1 − (<italic>x</italic> + <italic>c</italic> · <italic>u</italic>)<sup>2</sup>)<sup>2</sup> + (<italic>m</italic><sup>2</sup> − (<italic>a</italic><sup>2</sup> −′ 1) · <italic>l</italic><sup>2</sup> − 1)<sup>2</sup> + (<italic>k</italic> + <italic>i</italic> · (<italic>a</italic> − 1) − <italic>l</italic>)<sup>2</sup> + (<italic>n</italic> + <italic>l</italic> + <italic>v</italic> − <italic>y</italic>)<sup>2</sup> + (<italic>p</italic> + <italic>l</italic> · (<italic>a</italic> − <italic>n</italic> − 1) + <italic>b</italic> · (2 · <italic>a</italic> · (<italic>n</italic> + 1) − (<italic>n</italic> + 1)<sup>2</sup> − 1) − <italic>m</italic>)<sup>2</sup> + (<italic>q</italic> + <italic>y</italic> · (<italic>a</italic> − <italic>p</italic> − 1) + <italic>s</italic> · (2 · <italic>a</italic> · (<italic>p</italic> + 1) − (<italic>p</italic> + 1)<sup>2</sup> − 1) − <italic>x</italic>)<sup>2</sup> + (<italic>z</italic> + <italic>p</italic> · <italic>l</italic> · (<italic>a</italic> − <italic>p</italic>) + <italic>t</italic> · (2 · <italic>a</italic> · <italic>p</italic> − <italic>p</italic><sup>2</sup> − 1) − <italic>p</italic> · <italic>m</italic>)<sup>2</sup> and we prove that that for any positive integer <italic>k</italic> so that <italic>k</italic> + 1 is prime it is necessary and sufficient that there exist other natural variables <italic>a</italic>-<italic>z</italic> for which the polynomial equals zero. 26 variables is not the best known result in relation to the set of prime numbers, since any diophantine equation over ℕ can be reduced to one in 13 unknowns [8] or even less [5], [13]. The best currently known result for all prime numbers, where the polynomial is explicitly constructed is 10 [7] or even 7 in the case of Fermat as well as Mersenne prime number [4]. We are currently focusing our formalization efforts in this direction.</p>
</abstract>Quadratic Extensionshttps://sciendo.com/article/10.2478/forma-2021-0021<abstract>
<title style='display:none'>Summary</title>
<p>In this article we further develop field theory [6], [7], [12] in Mizar [1], [2], [3]: we deal with quadratic polynomials and quadratic extensions [5], [4]. First we introduce quadratic polynomials, their discriminants and prove the midnight formula. Then we show that - in case the discriminant of <italic>p</italic> being non square - adjoining a root of <italic>p</italic>’s discriminant results in a splitting field of <italic>p</italic>. Finally we prove that these are the only field extensions of degree 2, e.g. that an extension <italic>E</italic> of <italic>F</italic> is quadratic if and only if there is a non square Element <italic>a</italic> ∈ <italic>F</italic> such that <italic>E</italic> and (<inline-formula>
<alternatives>
<inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="graphic/j_forma-2021-0021_eq_001.png"/>
<mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"><mml:mrow><mml:mi>F</mml:mi><mml:msqrt><mml:mi>a</mml:mi></mml:msqrt></mml:mrow></mml:math>
<tex-math>F\sqrt a</tex-math>
</alternatives>
</inline-formula>) are isomorphic over <italic>F</italic>.</p>
</abstract>Duality Notions in Real Projective Planehttps://sciendo.com/article/10.2478/forma-2021-0016<abstract>
<title style='display:none'>Summary</title>
<p>In this article, we check with the Mizar system [1], [2], the converse of Desargues’ theorem and the converse of Pappus’ theorem of the real projective plane. It is well known that in the projective plane, the notions of points and lines are dual [11], [9], [15], [8]. Some results (analytical, synthetic, combinatorial) of projective geometry are already present in some libraries Lean/Hott [5], Isabelle/Hol [3], Coq [13], [14], [4], Agda [6], . . . .</p>
<p>Proofs of dual statements by proof assistants have already been proposed, using an axiomatic method (for example see in [13] - the section on duality: “[...] For every theorem we prove, we can easily derive its dual using our function swap [...]<sup>2</sup>”).</p>
<p>In our formalisation, we use an analytical rather than a synthetic approach using the definitions of Leończuk and Prażmowski of the projective plane [12]. Our motivation is to show that it is possible by developing dual definitions to find proofs of dual theorems in a few lines of code.</p>
<p>In the first part, rather technical, we introduce definitions that allow us to construct the duality between the points of the real projective plane and the lines associated to this projective plane. In the second part, we give a natural definition of line concurrency and prove that this definition is dual to the definition of alignment. Finally, we apply these results to find, in a few lines, the dual properties and theorems of those defined in the article [12] (transitive, Vebleian, at_least_3rank, Fanoian, Desarguesian, 2-dimensional).</p>
<p>We hope that this methodology will allow us to continued more quickly the proof started in [7] that the Beltrami-Klein plane is a model satisfying the axioms of the hyperbolic plane (in the sense of Tarski geometry [10]).</p>
</abstract>Automatization of Ternary Boolean Algebrashttps://sciendo.com/article/10.2478/forma-2021-0015<abstract>
<title style='display:none'>Summary</title>
<p>The main aim of this article is to introduce formally ternary Boolean algebras (TBAs) in terms of an abstract ternary operation, and to show their connection with the ordinary notion of a Boolean algebra, already present in the Mizar Mathematical Library [2]. Essentially, the core of this Mizar [1] formalization is based on the paper of A.A. Grau “Ternary Boolean Algebras” [7]. The main result is the single axiom for this class of lattices [12]. This is the continuation of the articles devoted to various equivalent axiomatizations of Boolean algebras: following Huntington [8] in terms of the binary sum and the complementation useful in the formalization of the Robbins problem [5], in terms of Sheffer stroke [9]. The classical definition ([6], [3]) can be found in [15] and its formalization is described in [4].</p>
<p>Similarly as in the case of recent formalizations of WA-lattices [14] and quasilattices [10], some of the results were proven in the Mizar system with the help of Prover9 [13], [11] proof assistant, so proofs are quite lengthy. They can be subject for subsequent revisions to make them more compact.</p>
</abstract>Algorithm NextFit for the Bin Packing Problemhttps://sciendo.com/article/10.2478/forma-2021-0014<abstract>
<p><bold>Summary</bold>. The bin packing problem is a fundamental and important optimization problem in theoretical computer science [4], [6]. An instance is a sequence of items, each being of positive size at most one. The task is to place all the items into bins so that the total size of items in each bin is at most one and the number of bins that contain at least one item is minimum.</p>
<p>Approximation algorithms have been intensively studied. Algorithm NextFit would be the simplest one. The algorithm repeatedly does the following: If the first unprocessed item in the sequence can be placed, in terms of size, additionally to the bin into which the algorithm has placed an item the last time, place the item into that bin; otherwise place the item into an empty bin. Johnson [5] proved that the number of the resulting bins by algorithm NextFit is less than twice the number of the fewest bins that are needed to contain all items.</p>
<p>In this article, we formalize in Mizar [1], [2] the bin packing problem as follows: An instance is a sequence of positive real numbers that are each at most one. The task is to find a function that maps the indices of the sequence to positive integers such that the sum of the subsequence for each of the inverse images is at most one and the size of the image is minimum. We then formalize algorithm NextFit, its feasibility, its approximation guarantee, and the tightness of the approximation guarantee.</p>
</abstract>Real Vector Space and Related Notionshttps://sciendo.com/article/10.2478/forma-2021-0012<abstract>
<p><bold>Summary</bold>. In this paper, we discuss the properties that hold in finite dimensional vector spaces and related spaces. In the Mizar language [1], [2], variables are strictly typed, and their type conversion requires a complicated process. Our purpose is to formalize that some properties of finite dimensional vector spaces are preserved in type transformations, and to contain the complexity of type transformations into this paper. Specifically, we show that properties such as algebraic structure, subsets, finite sequences and their sums, linear combination, linear independence, and affine independence are preserved in type conversions among <monospace>TOP-REAL(n)</monospace>, <monospace>REAL-NS(n)</monospace>, and <monospace>n-VectSp over F Real</monospace>. We referred to [4], [9], and [8] in the formalization.</p>
</abstract>Splitting Fieldshttps://sciendo.com/article/10.2478/forma-2021-0013<abstract>
<p><bold>Summary</bold>. In this article we further develop field theory in Mizar [1], [2]: we prove existence and uniqueness of splitting fields. We define the splitting field of a polynomial <italic>p</italic> ∈ <italic>F</italic> [<italic>X</italic>] as the smallest field extension of <italic>F</italic>, in which <italic>p</italic> splits into linear factors. From this follows, that for a splitting field <italic>E</italic> of <italic>p</italic> we have <italic>E</italic> = <italic>F</italic> (<italic>A</italic>) where <italic>A</italic> is the set of <italic>p</italic>’s roots. Splitting fields are unique, however, only up to isomorphisms; to be more precise up to <italic>F</italic> -isomorphims i.e. isomorphisms <italic>i</italic> with <italic>i|<sub>F</sub></italic> = Id<italic><sub>F</sub></italic>. We prove that two splitting fields of <italic>p</italic> ∈ <italic>F</italic> [<italic>X</italic>] are <italic>F</italic> -isomorphic using the well-known technique [4], [3] of extending isomorphisms from <italic>F</italic><sub>1</sub> → <italic>F</italic><sub>2</sub> to <italic>F</italic><sub>1</sub>(<italic>a</italic>) → <italic>F</italic><sub>2</sub>(<italic>b</italic>) for <italic>a</italic> and <italic>b</italic> being algebraic over <italic>F</italic><sub>1</sub> and <italic>F</italic><sub>2</sub>, respectively.</p>
</abstract>Some Properties of Membership Functions Composed of Triangle Functions and Piecewise Linear Functionshttps://sciendo.com/article/10.2478/forma-2021-0011<abstract>
<p><bold>Summary</bold>. IF-THEN rules in fuzzy inference is composed of multiple fuzzy sets (membership functions). IF-THEN rules can therefore be considered as a pair of membership functions [7]. The evaluation function of fuzzy control is composite function with fuzzy approximate reasoning and is functional on the set of membership functions. We obtained continuity of the evaluation function and compactness of the set of membership functions [12]. Therefore, we proved the existence of pair of membership functions, which maximizes (minimizes) evaluation function and is considered IF-THEN rules, in the set of membership functions by using extreme value theorem. The set of membership functions (fuzzy sets) is defined in this article to verifier our proofs before by Mizar [9], [10], [4]. Membership functions composed of triangle function, piecewise linear function and Gaussian function used in practice are formalized using existing functions.</p>
<p>On the other hand, not only curve membership functions mentioned above but also membership functions composed of straight lines (piecewise linear function) like triangular and trapezoidal functions are formalized. Moreover, different from the definition in [3] formalizations of triangular and trapezoidal function composed of two straight lines, minimum function and maximum functions are proposed. We prove, using the Mizar [2], [1] formalism, some properties of membership functions such as continuity and periodicity [13], [8].</p>
</abstract>On Primary Ideals. Part Ihttps://sciendo.com/article/10.2478/forma-2021-0010<abstract>
<p><bold>Summary</bold>. We formalize in the Mizar System [3], [4], definitions and basic propositions about primary ideals of a commutative ring along with Chapter 4 of [1] and Chapter III of [8]. Additionally other necessary basic ideal operations such as compatibilities taking radical and intersection of finite number of ideals are formalized as well in order to prove theorems relating primary ideals. These basic operations are mainly quoted from Chapter 1 of [1] and compiled as preliminaries in the first half of the article.</p>
</abstract>Ascoli-Arzelà Theoremhttps://sciendo.com/article/10.2478/forma-2021-0009<abstract>
<p><bold>Summary</bold>. In this article we formalize the Ascoli-Arzelà theorem [5], [6], [8] in Mizar [1], [2]. First, we gave definitions of equicontinuousness and equiboundedness of a set of continuous functions [12], [7], [3], [9]. Next, we formalized the Ascoli-Arzelà theorem using those definitions, and proved this theorem.</p>
</abstract>On Weakly Associative Lattices and Near Latticeshttps://sciendo.com/article/10.2478/forma-2021-0008<abstract>
<p><bold>Summary</bold>. The main aim of this article is to introduce formally two generalizations of lattices, namely weakly associative lattices and near lattices, which can be obtained from the former by certain weakening of the usual well-known axioms. We show selected propositions devoted to weakly associative lattices and near lattices from Chapter 6 of [15], dealing also with alternative versions of classical axiomatizations. Some of the results were proven in the Mizar [1], [2] system with the help of Prover9 [14] proof assistant.</p>
</abstract>Pappus’s Hexagon Theorem in Real Projective Planehttps://sciendo.com/article/10.2478/forma-2021-0007<abstract>
<p><bold>Summary</bold>. In this article we prove, using Mizar [2], [1], the Pappus’s hexagon theorem in the real projective plane: “Given one set of collinear points <italic>A, B, C</italic>, and another set of collinear points <italic>a, b, c</italic>, then the intersection points <italic>X, Y, Z</italic> of line pairs <italic>Ab</italic> and <italic>aB, Ac</italic> and <italic>aC, Bc</italic> and <italic>bC</italic> are collinear”<fn id="j_forma-2021-0007_fn_2" symbol="2"><p><ext-link ext-link-type="uri" xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="https://en.wikipedia.org/wiki/Pappus’s_hexagon_theorem">https://en.wikipedia.org/wiki/Pappus’s_hexagon_theorem</ext-link></p></fn>.</p>
<p>More precisely, we prove that the structure <monospace>ProjectiveSpace TOP-REAL3</monospace> [10] (where <monospace>TOP-REAL3</monospace> is a metric space defined in [5]) satisfies the Pappus’s axiom defined in [11] by Wojciech Leończuk and Krzysztof Prażmowski. Eugeniusz Kusak and Wojciech Leończuk formalized the Hessenberg theorem early in the MML [9]. With this result, the real projective plane is Desarguesian. For proving the Pappus’s theorem, two different proofs are given. First, we use the techniques developed in the section “Projective Proofs of Pappus’s Theorem” in the chapter “Pappos’s Theorem: Nine proofs and three variations” [12]. Secondly, Pascal’s theorem [4] is used.</p>
<p>In both cases, to prove some lemmas, we use <monospace>Prover9</monospace><fn id="j_forma-2021-0007_fn_3" symbol="3"><p><ext-link ext-link-type="uri" xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="https://www.cs.unm.edu/~mccune/prover9/">https://www.cs.unm.edu/~mccune/prover9/</ext-link></p></fn>, the successor of the <monospace>Otter</monospace> prover and <monospace>ott2miz</monospace> by Josef Urban<fn id="j_forma-2021-0007_fn_4" symbol="4"><p>See its homepage <ext-link ext-link-type="uri" xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="https://github.com/JUrban/ott2miz">https://github.com/JUrban/ott2miz</ext-link></p></fn> [13], [8], [7].</p>
<p>In <monospace>Coq</monospace>, the Pappus’s theorem is proved as the application of Grassmann-Cayley algebra [6] and more recently in Tarski’s geometry [3].</p>
</abstract>Functional Sequence in Norm Spacehttps://sciendo.com/article/10.2478/forma-2020-0023<abstract>
<title style='display:none'>Summary</title>
<p>In this article, we formalize in Mizar [1], [2] functional sequences and basic operations on functional sequences in norm space based on [5]. In the first section, we define functional sequence in norm space. In the second section, we define pointwise convergence and prove some related theorems. In the last section we define uniform convergence and limit of functional sequence.</p>
</abstract>Partial Correctness of an Algorithm Computing Lucas Sequenceshttps://sciendo.com/article/10.2478/forma-2020-0025<abstract>
<title style='display:none'>Summary</title>
<p>In this paper we define some properties about finite sequences and verify the partial correctness of an algorithm computing <italic>n</italic>-th element of Lucas sequence [23], [20] with given <italic>P</italic> and <italic>Q</italic> coefficients as well as two first elements (<italic>x</italic> and <italic>y</italic>). The algorithm is encoded in nominative data language [22] in the Mizar system [3], [1].</p>
<p><disp-quote><p><monospace>i := 0</monospace></p>
<p><monospace>s := x</monospace></p>
<p><monospace>b := y</monospace></p>
<p><monospace>c := x</monospace></p>
<p><monospace>while (i <> n)</monospace></p>
<p> <monospace>c := s</monospace></p>
<p> <monospace>s := b</monospace></p>
<p> <monospace>ps := p*s</monospace></p>
<p> <monospace>qc := q*c</monospace></p>
<p> <monospace>b := ps − qc</monospace></p>
<p> <monospace>i := i + j</monospace></p>
<p><monospace>return s</monospace></p></disp-quote></p>
<p>This paper continues verification of algorithms [10], [14], [12], [15], [13] written in terms of simple-named complex-valued nominative data [6], [8], [19], [11], [16], [17]. The validity of the algorithm is presented in terms of semantic Floyd-Hoare triples over such data [9]. Proofs of the correctness are based on an inference system for an extended Floyd-Hoare logic [2], [4] with partial pre- and post-conditions [18], [21], [7], [5].</p>
</abstract>en-us-1