<abstract><title style='display:none'>Summary</title>In this article, using the Mizar system [2], [1], we discuss invertible operators on Banach spaces. In the first chapter, we formalized the theorem that denotes any operators that are close enough to an invertible operator are also invertible by using the property of Neumann series.In the second chapter, we formalized the continuity of an isomorphism that maps an invertible operator on Banach spaces to its inverse. These results are used in the proof of the implicit function theorem. We referred to [3], [10], [6], [7] in this formalization.</abstract>

Invertible Operators on Banach Spaces

<abstract><title style='display:none'>Summary</title>The binary set {0, 1} together with modulo-2 addition and multiplication is called a binary field, which is denoted by F2. The binary field F2 is defined in [1]. A vector space over F2 is called a binary vector space. The set of all binary vectors of length n forms an n-dimensional vector space Vn over F2. Binary fields and n-dimensional binary vector spaces play an important role in practical computer science, for example, coding theory [15] and cryptology. In cryptology, binary fields and n-dimensional binary vector spaces are very important in proving the security of cryptographic systems [13]. In this article we define the n-dimensional binary vector space Vn. Moreover, we formalize some facts about the n-dimensional binary vector space Vn.</abstract>

This research was presented during the 2013 International Conference on Foundations of
Computer Science FCS’13 in Las Vegas, USA

N-Dimensional Binary Vector Spaces

<abstract><title style='display:none'>Summary</title>We start with the definition of stopping time according to [<xref ref-type="bibr" rid="j_forma-2017-0010_ref_004_w2aab3b7b2b1b6b1ab1ab4Aa">4</xref>], p.283. We prove, that different definitions for stopping time can coincide. We give examples of stopping time using constant-functions or functions defined with the operator max or min (defined in [<xref ref-type="bibr" rid="j_forma-2017-0010_ref_006_w2aab3b7b2b1b6b1ab1ab6Aa">6</xref>], pp.37–38). Finally we give an example with some given filtration. Stopping time is very important for stochastic finance. A stopping time is the moment, where a certain event occurs ([<xref ref-type="bibr" rid="j_forma-2017-0010_ref_007_w2aab3b7b2b1b6b1ab1ab7Aa">7</xref>], p.372) and can be used together with stochastic processes ([<xref ref-type="bibr" rid="j_forma-2017-0010_ref_004_w2aab3b7b2b1b6b1ab1ab4Aa">4</xref>], p.283). Look at the following example: we install a function ST: {1,2,3,4} → {0, 1, 2} ∪ {+∞}, we define:a. ST(1)=1, ST(2)=1, ST(3)=2, ST(4)=2.b. The set {0,1,2} consists of time points: 0=now,1=tomorrow,2=the day after tomorrow.We can prove:c. {w, where w is Element of Ω: ST.w=0}=∅ &amp; {w, where w is Element of Ω: ST.w=1}={1,2} &amp; {w, where w is Element of Ω: ST.w=2}={3,4} andST is a stopping time.We use a function Filt as Filtration of {0,1,2}, Σ where Filt(0)=Ω<italic>now</italic>, Filt(1)=Ω<italic>fut</italic>1 and Filt(2)=Ω<italic>fut</italic>2. From a., b. and c. we know that:d. {w, where w is Element of Ω: ST.w=0} in Ω<italic>now</italic> and{w, where w is Element of Ω: ST.w=1} in Ω<italic>fut</italic>1 and{w, where w is Element of Ω: ST.w=2} in Ω<italic>fut</italic>2.The sets in d. are events, which occur at the time points 0(=now), 1(=tomorrow) or 2(=the day after tomorrow), see also [<xref ref-type="bibr" rid="j_forma-2017-0010_ref_007_w2aab3b7b2b1b6b1ab1ab7Aa">7</xref>], p.371. Suppose we have ST(1)=+∞, then this means that for 1 the corresponding event never occurs.As an interpretation for our installed functions consider the given adapted stochastic process in the article [<xref ref-type="bibr" rid="j_forma-2017-0010_ref_005_w2aab3b7b2b1b6b1ab1ab5Aa">5</xref>].ST(1)=1 means, that the given element 1 in {1,2,3,4} is stopped in 1 (=tomorrow). That tells us, that we have to look at the value <italic>f</italic>2(1) which is equal to 80. The same argumentation can be applied for the element 2 in {1,2,3,4}.ST(3)=2 means, that the given element 3 in {1,2,3,4} is stopped in 2 (=the day after tomorrow). That tells us, that we have to look at the value <italic>f</italic>3(3) which is equal to 100.ST(4)=2 means, that the given element 4 in {1,2,3,4} is stopped in 2 (=the day after tomorrow). That tells us, that we have to look at the value <italic>f</italic>3(4) which is equal to 120.In the real world, these functions can be used for questions like: when does the share price exceed a certain limit? (see [<xref ref-type="bibr" rid="j_forma-2017-0010_ref_007_w2aab3b7b2b1b6b1ab1ab7Aa">7</xref>], p.372).</abstract>

Introduction to Stopping Time in Stochastic Finance Theory

<abstract><title style='display:none'>Summary</title>We first provide a modified version of the proof in [3] that
the Sorgenfrey line is <italic>T</italic>1. Here, we prove that it is in fact T2, a stronger result.
Next, we prove that all subspaces of ℝ1 (that is the real line with the usual
topology) are Lindel¨of. We utilize this result in the proof that the Sorgenfrey
line is Lindel¨of, which is based on the proof found in [8]. Next, we construct the
Sorgenfrey plane, as the product topology of the Sorgenfrey line and itself. We
prove that the Sorgenfrey plane is not Lindel¨of, and therefore the product space
of two Lindel¨of spaces need not be Lindel¨of. Further, we note that the Sorgenfrey
line is regular, following from [3]:59. Next, we observe that the Sorgenfrey line is
normal since it is both regular and Lindel¨of. Finally, we prove that the Sorgenfrey
plane is not normal, and hence the product of two normal spaces need not be
normal. The proof that the Sorgenfrey plane is not normal and many of the
lemmas leading up to this result are modelled after the proof in [3], that the
Niemytzki plane is not normal. Information was also gathered from [15].</abstract>

Some Properties of the Sorgenfrey Line and the Sorgenfrey Plane

<abstract xml:lang="en"><title style='display:none'>Affine Independence in Vector Spaces</title>In this article we describe the notion of affinely independent subset of a real linear space. First we prove selected theorems concerning operations on linear combinations. Then we introduce affine independence and prove the equivalence of various definitions of this notion. We also introduce the notion of the affine hull, i.e. a subset generated by a set of vectors which is an intersection of all affine sets including the given set. Finally, we introduce and prove selected properties of the barycentric coordinates.</abstract>

Affine Independence in Vector Spaces

<abstract><title style='display:none'>Summary.</title>The article continues the formalization of the lattice theory (as structures with two binary operations, not in terms of ordering relations). In the Mizar Mathematical Library, there are some attempts to formalize prime ideals and filters; one series of articles written as decoding [9] proven some results; we tried however to follow [21], [12], and [13]. All three were devoted to the Stone representation theorem [18] for Boolean or Heyting lattices. The main aim of the present article was to bridge this gap between general distributive lattices and Boolean algebras, having in mind that the more general approach will eventually replace the common proof of aforementioned articles.1 Because in Boolean algebras the notions of ultrafilters, prime filters and maximal filters coincide, we decided to construct some concrete examples of ultrafilters in nontrivial Boolean lattice. We proved also the Prime Ideal Theorem not as BPI (Boolean Prime Ideal), but in the more general setting. In the final section we present Nachbin theorems [15],[1] expressed both in terms of maximal and prime filters and as the unordered spectra of a lattice [11], [10]. This shows that if the notion of maximal and prime filters coincide in the lattice, it is Boolean.</abstract>

Prime Filters and Ideals in Distributive Lattices

<abstract><title style='display:none'>Summary</title>In [3] the existence of the Cantor normal form of ordinals was proven in the Mizar system [6]. In this article its uniqueness is proven and then used to formalize the natural sum of ordinals.</abstract>

Natural Addition of Ordinals

<abstract><title style='display:none'>Summary</title>This article is the final step of our attempts to formalize the negative solution of Hilbert’s tenth problem.In our approach, we work with the Pell’s Equation defined in [2]. We analyzed this equation in the general case to show its solvability as well as the cardinality and shape of all possible solutions. Then we focus on a special case of the equation, which has the form <italic>x</italic>2<italic>−</italic> (<italic>a</italic>2 − 1)<italic>y</italic>2 = 1 [8] and its solutions considered as two sequences <inline-formula><alternatives><inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="graphic/j_forma-2019-0020_eq_001.png"/><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"><mml:mrow><mml:msubsup><mml:mrow><mml:mrow><mml:mrow><mml:mo>{</mml:mo><mml:mrow><mml:msub><mml:mrow><mml:mi>x</mml:mi></mml:mrow><mml:mi>i</mml:mi></mml:msub><mml:mo>(</mml:mo><mml:mi>a</mml:mi><mml:mo>)</mml:mo></mml:mrow><mml:mo>}</mml:mo></mml:mrow></mml:mrow></mml:mrow><mml:mrow><mml:mi>i</mml:mi><mml:mo>=</mml:mo><mml:mn>0</mml:mn></mml:mrow><mml:mo>∞</mml:mo></mml:msubsup><mml:mo>,</mml:mo><mml:msubsup><mml:mrow><mml:mrow><mml:mrow><mml:mo>{</mml:mo><mml:mrow><mml:msub><mml:mrow><mml:mi>y</mml:mi></mml:mrow><mml:mi>i</mml:mi></mml:msub><mml:mo>(</mml:mo><mml:mi>a</mml:mi><mml:mo>)</mml:mo></mml:mrow><mml:mo>}</mml:mo></mml:mrow></mml:mrow></mml:mrow><mml:mrow><mml:mi>i</mml:mi><mml:mo>=</mml:mo><mml:mn>0</mml:mn></mml:mrow><mml:mo>∞</mml:mo></mml:msubsup></mml:mrow></mml:math><tex-math>$\left\{ {{x_i}(a)} \right\}_{i = 0}^\infty ,\left\{ {{y_i}(a)} \right\}_{i = 0}^\infty$</tex-math></alternatives></inline-formula>. We showed in [1] that the <italic>n</italic>-th element of these sequences can be obtained from lists of several basic Diophantine relations as linear equations, finite products, congruences and inequalities, or more precisely that the equation <italic>x</italic> = <italic>y</italic>i(<italic>a</italic>) is Diophantine. Following the post-Matiyasevich results we show that the equality determined by the value of the power function <italic>y</italic> = <italic>x</italic>z is Diophantine, and analogously property in cases of the binomial coe cient, factorial and several product [9].In this article, we combine analyzed so far Diophantine relation using conjunctions, alternatives as well as substitution to prove the bounded quantifier theorem. Based on this theorem we prove MDPR-theorem that <italic>every recursively enumerable set is Diophantine,</italic> where recursively enumerable sets have been defined by the Martin Davis normal form.The formalization by means of Mizar system [5], [7], [4] follows [10], Z. Adamowicz, P. Zbierski [3] as well as M. Davis [6].</abstract>

Formalization of the MRDP Theorem in the Mizar System

<abstract>
<title style='display:none'>Summary</title>
This is Erdős’s proof of the divergence of the sum of prime reciprocals, using the Mizar system [2], [3], as reported in “Proofs from THE BOOK” [1].
</abstract>

The Divergence of the Sum of Prime Reciprocals

<abstract>
<title style='display:none'>Summary</title>
Conway’s introduction to algebraic operations on surreal numbers with a rather simple definition. However, he combines recursion with Conway’s induction on surreal numbers, more formally he combines transfinite induction-recursion with the properties of proper classes, which is diffcult to introduce formally.
This article represents a further step in our ongoing e orts to investigate the possibilities offered by Mizar with Tarski-Grothendieck set theory [<xref ref-type="bibr" rid="j_forma-2023-0020_ref_004">4</xref>] to introduce the algebraic structure of Conway numbers and to prove their ring character.
</abstract>

The Ring of Conway Numbers in Mizar

<abstract>
<title style='display:none'>Summary</title>
In this paper we present the Mizar formalization of the 36th problem from W. Sierpiński’s book “250 Problems in Elementary Number Theory” [<xref ref-type="bibr" rid="j_forma-2023-0021_ref_010">10</xref>].
</abstract>

Elementary Number Theory Problems. Part XI

<abstract>
<title style='display:none'>Summary</title>
In the article, we continue the formalization of the work devoted to Tarski’s geometry – the book “Metamathematische Methoden in der Geometrie” by W. Schwabhäuser, W. Szmielew, and A. Tarski. We use the Mizar system to formalize Chapter 9 of this book. We deal with half-planes and planes proving their properties as well as the theory of intersecting lines.
</abstract>

Tarski Geometry Axioms. Part V – Half-planes and Planes

<abstract>
<title style='display:none'>Summary</title>
This paper continues the formalization of problems defined in the book “250 Problems in Elementary Number Theory” by Wacław Sierpiński.
</abstract>

Elementary Number Theory Problems. Part X – Diophantine Equations

<abstract>
<title style='display:none'>Summary</title>
Surreal numbers, a fascinating mathematical concept introduced by John Conway, have attracted considerable interest due to their unique properties. In this article, we formalize the basic concept of surreal numbers close to the original Conway’s convention in the field of combinatorial game theory. We define surreal numbers with the pre-order in the Mizar system which satisfy the following condition: <italic>x</italic> ⩽ <italic>y</italic> iff <italic>Lx</italic> ≪ {<italic>y</italic>} <italic>Λ</italic> {<italic>x</italic>} ≪ <italic>Ry</italic>.
</abstract>

Conway Numbers – Formal Introduction

<abstract>
<title style='display:none'>Summary</title>
In this article, we develop our formalised concept of Conway numbers as outlined in [<xref ref-type="bibr" rid="j_forma-2023-0019_ref_009">9</xref>]. We focus mainly pre-order properties, birthday arithmetic contained in the Chapter 1, <italic>Properties of Order and Equality</italic> of John Conway’s seminal book. We also propose a method for the selection of class representatives respecting the relation defined by the pre-ordering in order to facilitate combining the results obtained for the original and tree-theoretic definitions of Conway numbers.
</abstract>

Integration of Game Theoretic and Tree Theoretic Approaches to Conway Numbers

<abstract>
<title style='display:none'>Summary</title>
This paper introduces multidimensional measure spaces and the integration of functions on these spaces in Mizar. Integrals on the multidimensional Cartesian product measure space are defined and appropriate formal apparatus to deal with this notion is provided as well.
</abstract>

Multidimensional Measure Space and Integration

<abstract><title style='display:none'>Summary</title>In <xref ref-type="bibr" rid="j_forma-2016-0010_ref_021_w2aab2b8b7b1b7b1ab1ac21Aa">[21]</xref>, Marco Riccardi formalized that ℝN-basis <italic>n</italic> is a basis (in the algebraic sense defined in <xref ref-type="bibr" rid="j_forma-2016-0010_ref_026_w2aab2b8b7b1b7b1ab1ac26Aa">[26]</xref>) of <inline-formula><alternatives><inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="graphic/j_forma-2016-0010_eq_001.png"/><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"><mml:mrow><mml:msubsup><mml:mi>ℰ</mml:mi><mml:mi>T</mml:mi><mml:mi>n</mml:mi></mml:msubsup></mml:mrow></mml:math><tex-math>${\cal E}_T^n $</tex-math></alternatives></inline-formula> and in <xref ref-type="bibr" rid="j_forma-2016-0010_ref_020_w2aab2b8b7b1b7b1ab1ac20Aa">[20]</xref> he has formalized that <inline-formula><alternatives><inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="graphic/j_forma-2016-0010_eq_001.png"/><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"><mml:mrow><mml:msubsup><mml:mi>ℰ</mml:mi><mml:mi>T</mml:mi><mml:mi>n</mml:mi></mml:msubsup></mml:mrow></mml:math><tex-math>${\cal E}_T^n $</tex-math></alternatives></inline-formula> is second-countable, we build (in the topological sense defined in <xref ref-type="bibr" rid="j_forma-2016-0010_ref_023_w2aab2b8b7b1b7b1ab1ac23Aa">[23]</xref>) a denumerable base of <inline-formula><alternatives><inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="graphic/j_forma-2016-0010_eq_001.png"/><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"><mml:mrow><mml:msubsup><mml:mi>ℰ</mml:mi><mml:mi>T</mml:mi><mml:mi>n</mml:mi></mml:msubsup></mml:mrow></mml:math><tex-math>${\cal E}_T^n $</tex-math></alternatives></inline-formula>.Then we introduce the <italic>n</italic>-dimensional intervals (interval in <italic>n</italic>-dimensional Euclidean space, <italic>pavé (borné) de</italic> ℝ<italic>n</italic><xref ref-type="bibr" rid="j_forma-2016-0010_ref_016_w2aab2b8b7b1b7b1ab1ac16Aa">[16]</xref>, <italic>semi-intervalle (borné) de</italic> ℝ<italic>n</italic><xref ref-type="bibr" rid="j_forma-2016-0010_ref_022_w2aab2b8b7b1b7b1ab1ac22Aa">[22]</xref>).We conclude with the definition of Chebyshev distance <xref ref-type="bibr" rid="j_forma-2016-0010_ref_011_w2aab2b8b7b1b7b1ab1ac11Aa">[11]</xref>.</abstract>

Chebyshev Distance

<abstract><title style='display:none'>Summary</title>We show that the set of all partial predicates over a set <italic>D</italic> together with the disjunction, conjunction, and negation operations, defined in accordance with the truth tables of S.C. Kleene’s strong logic of indeterminacy [<xref ref-type="bibr" rid="j_forma-2018-0002_ref_017_w2aab3b7b1b1b6b1ab1ac17Aa">17</xref>], forms a Kleene algebra. A Kleene algebra is a De Morgan algebra [<xref ref-type="bibr" rid="j_forma-2018-0002_ref_003_w2aab3b7b1b1b6b1ab1ab3Aa">3</xref>] (also called quasi-Boolean algebra) which satisfies the condition <italic>x</italic> ∧<italic>¬:x</italic> ⩽ <italic>y</italic> ∨<italic>¬ :y</italic> (sometimes called the normality axiom). We use the formalization of De Morgan algebras from [<xref ref-type="bibr" rid="j_forma-2018-0002_ref_008_w2aab3b7b1b1b6b1ab1ab8Aa">8</xref>].The term “Kleene algebra” was introduced by A. Monteiro and D. Brignole in [<xref ref-type="bibr" rid="j_forma-2018-0002_ref_003_w2aab3b7b1b1b6b1ab1ab3Aa">3</xref>]. A similar notion of a “normal i-lattice” had been previously studied by J.A. Kalman [<xref ref-type="bibr" rid="j_forma-2018-0002_ref_016_w2aab3b7b1b1b6b1ab1ac16Aa">16</xref>]. More details about the origin of this notion and its relation to other notions can be found in [<xref ref-type="bibr" rid="j_forma-2018-0002_ref_024_w2aab3b7b1b1b6b1ab1ac24Aa">24</xref>, <xref ref-type="bibr" rid="j_forma-2018-0002_ref_004_w2aab3b7b1b1b6b1ab1ab4Aa">4</xref>, <xref ref-type="bibr" rid="j_forma-2018-0002_ref_001_w2aab3b7b1b1b6b1ab1ab1Aa">1</xref>, <xref ref-type="bibr" rid="j_forma-2018-0002_ref_002_w2aab3b7b1b1b6b1ab1ab2Aa">2</xref>]. It should be noted that there is a different widely known class of algebras, also called Kleene algebras [<xref ref-type="bibr" rid="j_forma-2018-0002_ref_022_w2aab3b7b1b1b6b1ab1ac22Aa">22</xref>, <xref ref-type="bibr" rid="j_forma-2018-0002_ref_006_w2aab3b7b1b1b6b1ab1ab6Aa">6</xref>], which generalize the algebra of regular expressions, however, the term “Kleene algebra” used in this paper does not refer to them.Algebras of partial predicates naturally arise in computability theory in the study on partial recursive predicates. They were studied in connection with non-classical logics [<xref ref-type="bibr" rid="j_forma-2018-0002_ref_017_w2aab3b7b1b1b6b1ab1ac17Aa">17</xref>, <xref ref-type="bibr" rid="j_forma-2018-0002_ref_005_w2aab3b7b1b1b6b1ab1ab5Aa">5</xref>, <xref ref-type="bibr" rid="j_forma-2018-0002_ref_018_w2aab3b7b1b1b6b1ab1ac18Aa">18</xref>, <xref ref-type="bibr" rid="j_forma-2018-0002_ref_032_w2aab3b7b1b1b6b1ab1ac32Aa">32</xref>, <xref ref-type="bibr" rid="j_forma-2018-0002_ref_029_w2aab3b7b1b1b6b1ab1ac29Aa">29</xref>, <xref ref-type="bibr" rid="j_forma-2018-0002_ref_030_w2aab3b7b1b1b6b1ab1ac30Aa">30</xref>]. A partial predicate also corresponds to the notion of a partial set [<xref ref-type="bibr" rid="j_forma-2018-0002_ref_026_w2aab3b7b1b1b6b1ab1ac26Aa">26</xref>] on a given domain, which represents a (partial) property which for any given element of this domain may hold, not hold, or neither hold nor not hold. The field of all partial sets on a given domain is an algebra with generalized operations of union, intersection, complement, and three constants (0, 1, <italic>n</italic> which is the fixed point of complement) which can be generalized to an equational class of algebras called DMF-algebras (De Morgan algebras with a single fixed point of involution) [<xref ref-type="bibr" rid="j_forma-2018-0002_ref_025_w2aab3b7b1b1b6b1ab1ac25Aa">25</xref>]. In [<xref ref-type="bibr" rid="j_forma-2018-0002_ref_027_w2aab3b7b1b1b6b1ab1ac27Aa">27</xref>] partial sets and DMF-algebras were considered as a basis for unification of set-theoretic and linguistic approaches to probability.Partial predicates over classes of mathematical models of data were used for formalizing semantics of computer programs in the composition-nominative approach to program formalization [<xref ref-type="bibr" rid="j_forma-2018-0002_ref_031_w2aab3b7b1b1b6b1ab1ac31Aa">31</xref>, <xref ref-type="bibr" rid="j_forma-2018-0002_ref_028_w2aab3b7b1b1b6b1ab1ac28Aa">28</xref>, <xref ref-type="bibr" rid="j_forma-2018-0002_ref_033_w2aab3b7b1b1b6b1ab1ac33Aa">33</xref>, <xref ref-type="bibr" rid="j_forma-2018-0002_ref_015_w2aab3b7b1b1b6b1ab1ac15Aa">15</xref>], for formalizing extensions of the Floyd-Hoare logic [<xref ref-type="bibr" rid="j_forma-2018-0002_ref_007_w2aab3b7b1b1b6b1ab1ab7Aa">7</xref>, <xref ref-type="bibr" rid="j_forma-2018-0002_ref_009_w2aab3b7b1b1b6b1ab1ab9Aa">9</xref>] which allow reasoning about properties of programs in the case of partial pre- and postconditions [<xref ref-type="bibr" rid="j_forma-2018-0002_ref_023_w2aab3b7b1b1b6b1ab1ac23Aa">23</xref>, <xref ref-type="bibr" rid="j_forma-2018-0002_ref_020_w2aab3b7b1b1b6b1ab1ac20Aa">20</xref>, <xref ref-type="bibr" rid="j_forma-2018-0002_ref_019_w2aab3b7b1b1b6b1ab1ac19Aa">19</xref>, <xref ref-type="bibr" rid="j_forma-2018-0002_ref_021_w2aab3b7b1b1b6b1ab1ac21Aa">21</xref>], for formalizing dynamical models with partial behaviors in the context of the mathematical systems theory [<xref ref-type="bibr" rid="j_forma-2018-0002_ref_011_w2aab3b7b1b1b6b1ab1ac11Aa">11</xref>, <xref ref-type="bibr" rid="j_forma-2018-0002_ref_013_w2aab3b7b1b1b6b1ab1ac13Aa">13</xref>, <xref ref-type="bibr" rid="j_forma-2018-0002_ref_014_w2aab3b7b1b1b6b1ab1ac14Aa">14</xref>, <xref ref-type="bibr" rid="j_forma-2018-0002_ref_012_w2aab3b7b1b1b6b1ab1ac12Aa">12</xref>, <xref ref-type="bibr" rid="j_forma-2018-0002_ref_010_w2aab3b7b1b1b6b1ab1ac10Aa">10</xref>].</abstract>

Kleene Algebra of Partial Predicates

<abstract xml:lang="en"><title style='display:none'>Partial Differentiation on Normed Linear Spaces <italic>Rn</italic></title>Summary. In this article, we define the partial differentiation of functions of real variable and prove the linearity of this operator [18].</abstract>

Gifu National College of Technology, Japan

Partial Differentiation on Normed Linear Spaces <italic>Rn</italic>

<abstract><title style='display:none'>Summary</title>In this paper we give a formal definition of the notion of nominative data with simple names and complex values [<xref ref-type="bibr" rid="j_forma-2017-0020_ref_015_w2aab3b7b4b1b6b1ab1ac15Aa">15</xref>, <xref ref-type="bibr" rid="j_forma-2017-0020_ref_016_w2aab3b7b4b1b6b1ab1ac16Aa">16</xref>, <xref ref-type="bibr" rid="j_forma-2017-0020_ref_019_w2aab3b7b4b1b6b1ab1ac19Aa">19</xref>] and formal definitions of the basic operations on such data, including naming, denaming and overlapping, following the work [<xref ref-type="bibr" rid="j_forma-2017-0020_ref_019_w2aab3b7b4b1b6b1ab1ac19Aa">19</xref>].The notion of nominative data plays an important role in the composition-nominative approach to program formalization [<xref ref-type="bibr" rid="j_forma-2017-0020_ref_015_w2aab3b7b4b1b6b1ab1ac15Aa">15</xref>, <xref ref-type="bibr" rid="j_forma-2017-0020_ref_016_w2aab3b7b4b1b6b1ab1ac16Aa">16</xref>] which is a development of composition programming [<xref ref-type="bibr" rid="j_forma-2017-0020_ref_018_w2aab3b7b4b1b6b1ab1ac18Aa">18</xref>]. Both approaches are compared in [<xref ref-type="bibr" rid="j_forma-2017-0020_ref_014_w2aab3b7b4b1b6b1ab1ac14Aa">14</xref>].The composition-nominative approach considers mathematical models of computer software and data on various levels of abstraction and generality and provides mathematical tools for reasoning about their properties. In particular, nominative data are mathematical models of data which are stored and processed in computer systems. The composition-nominative approach considers different types [<xref ref-type="bibr" rid="j_forma-2017-0020_ref_014_w2aab3b7b4b1b6b1ab1ac14Aa">14</xref>, <xref ref-type="bibr" rid="j_forma-2017-0020_ref_019_w2aab3b7b4b1b6b1ab1ac19Aa">19</xref>] of nominative data, but all of them are based on the name-value relation. One powerful type of nominative data, which is suitable for representing many kinds of data commonly used in programming like lists, multidimensional arrays, trees, tables, etc. is the type of nominative data with simple (abstract) names and complex (structured) values. The set of nominative data of given type together with a number of basic operations on them like naming, denaming and overlapping [<xref ref-type="bibr" rid="j_forma-2017-0020_ref_019_w2aab3b7b4b1b6b1ab1ac19Aa">19</xref>] form an algebra which is called <italic>data algebra</italic>.In the composition-nominative approach computer programs which process data are modeled as partial functions which map nominative data from the carrier of a given data algebra (input data) to nominative data (output data). Such functions are also called <italic>binominative functions</italic>. Programs which evaluate conditions are modeled as partial predicates on nominative data (nominative predicates). Programming language constructs like sequential execution, branching, cycle, etc. which construct programs from the existing programs are modeled as operations which take binominative functions and predicates and produce binominative functions. Such operations are called <italic>compositions</italic>. A set of binominative functions and a set of predicates together with appropriate compositions form an algebra which is called <italic>program algebra</italic>. This algebra serves as a semantic model of a programming language.For functions over nominative data a special computability called abstract computability is introduces and complete classes of computable functions are specified [<xref ref-type="bibr" rid="j_forma-2017-0020_ref_016_w2aab3b7b4b1b6b1ab1ac16Aa">16</xref>].For reasoning about properties of programs modeled as binominative functions a Floyd-Hoare style logic [<xref ref-type="bibr" rid="j_forma-2017-0020_ref_001_w2aab3b7b4b1b6b1ab1ab1Aa">1</xref>, <xref ref-type="bibr" rid="j_forma-2017-0020_ref_002_w2aab3b7b4b1b6b1ab1ab2Aa">2</xref>] is introduced and applied [<xref ref-type="bibr" rid="j_forma-2017-0020_ref_012_w2aab3b7b4b1b6b1ab1ac12Aa">12</xref>, <xref ref-type="bibr" rid="j_forma-2017-0020_ref_013_w2aab3b7b4b1b6b1ab1ac13Aa">13</xref>, <xref ref-type="bibr" rid="j_forma-2017-0020_ref_008_w2aab3b7b4b1b6b1ab1ab8Aa">8</xref>, <xref ref-type="bibr" rid="j_forma-2017-0020_ref_011_w2aab3b7b4b1b6b1ab1ac11Aa">11</xref>, <xref ref-type="bibr" rid="j_forma-2017-0020_ref_009_w2aab3b7b4b1b6b1ab1ab9Aa">9</xref>, <xref ref-type="bibr" rid="j_forma-2017-0020_ref_010_w2aab3b7b4b1b6b1ab1ac10Aa">10</xref>]. One advantage of this approach to reasoning about programs is that it naturally handles programs which process complex data structures (which can be quite straightforwardly represented as nominative data). Also, unlike classical Floyd-Hoare logic, the mentioned logic allows reasoning about assertions which include partial pre- and post-conditions [<xref ref-type="bibr" rid="j_forma-2017-0020_ref_011_w2aab3b7b4b1b6b1ab1ac11Aa">11</xref>].Besides modeling data processed by programs, nominative data can be also applied to modeling data processed by signal processing systems in the context of the mathematical systems theory [<xref ref-type="bibr" rid="j_forma-2017-0020_ref_004_w2aab3b7b4b1b6b1ab1ab4Aa">4</xref>, <xref ref-type="bibr" rid="j_forma-2017-0020_ref_006_w2aab3b7b4b1b6b1ab1ab6Aa">6</xref>, <xref ref-type="bibr" rid="j_forma-2017-0020_ref_007_w2aab3b7b4b1b6b1ab1ab7Aa">7</xref>, <xref ref-type="bibr" rid="j_forma-2017-0020_ref_005_w2aab3b7b4b1b6b1ab1ab5Aa">5</xref>, <xref ref-type="bibr" rid="j_forma-2017-0020_ref_003_w2aab3b7b4b1b6b1ab1ab3Aa">3</xref>].</abstract>

Simple-Named Complex-Valued Nominative Data – Definition and Basic Operations

<abstract xml:lang="en"><title style='display:none'>Arrow's Impossibility Theorem</title>A formalization of the first proof from [6].</abstract>

Arrow's Impossibility Theorem

<abstract xml:lang="en"><title style='display:none'>Several Differentiation Formulas of Special Functions. Part V</title>In this article, we give several differentiation formulas of special and composite functions including trigonometric, polynomial and logarithmic functions.</abstract>

Several Differentiation Formulas of Special Functions. Part V

Editorial Policy

Open Access License

Publication Ethics Statement

Formalized Mathematics

(a computer assisted approach)

  Pioneering Journal in the field of formalized and mechanically checked mathematics. Excellent articles on latest research in formal methods and computer-checked...

Impact Factor

Five Year Impact Factor

MNiSW

Google Scholar h5-index

Google Scholar h5-median

  Pioneering Journal in the field of formalized and mechanically checked mathematics. Excellent articles on latest research in...