Issues

Journal & Issues

Volume 29 (2021): Issue 4 (December 2021)

Volume 29 (2021): Issue 3 (October 2021)

Volume 29 (2021): Issue 2 (July 2021)

Volume 29 (2021): Issue 1 (April 2021)

Volume 28 (2020): Issue 4 (December 2020)

Volume 28 (2020): Issue 3 (October 2020)

Volume 28 (2020): Issue 2 (July 2020)

Volume 28 (2020): Issue 1 (April 2020)

Volume 27 (2019): Issue 4 (December 2019)

Volume 27 (2019): Issue 3 (October 2019)

Volume 27 (2019): Issue 2 (July 2019)

Volume 27 (2019): Issue 1 (April 2019)

Volume 26 (2018): Issue 4 (December 2018)

Volume 26 (2018): Issue 3 (October 2018)

Volume 26 (2018): Issue 2 (July 2018)

Volume 26 (2018): Issue 1 (April 2018)

Volume 25 (2017): Issue 4 (December 2017)

Volume 25 (2017): Issue 3 (October 2017)

Volume 25 (2017): Issue 2 (July 2017)

Volume 25 (2017): Issue 1 (March 2017)

Volume 24 (2016): Issue 4 (December 2016)

Volume 24 (2016): Issue 3 (September 2016)

Volume 24 (2016): Issue 2 (June 2016)

Volume 24 (2016): Issue 1 (March 2016)

Volume 23 (2015): Issue 4 (December 2015)

Volume 23 (2015): Issue 3 (September 2015)

Volume 23 (2015): Issue 2 (June 2015)

Volume 23 (2015): Issue 1 (March 2015)

Volume 22 (2014): Issue 4 (December 2014)

Volume 22 (2014): Issue 3 (September 2014)

Volume 22 (2014): Issue 2 (June 2014)
Special Issue: 25 years of the Mizar Mathematical Library

Volume 22 (2014): Issue 1 (March 2014)

Volume 21 (2013): Issue 4 (December 2013)

Volume 21 (2013): Issue 3 (October 2013)

Volume 21 (2013): Issue 2 (June 2013)

Volume 21 (2013): Issue 1 (January 2013)

Volume 20 (2012): Issue 4 (December 2012)

Volume 20 (2012): Issue 3 (September 2012)

Volume 20 (2012): Issue 2 (June 2012)

Volume 20 (2012): Issue 1 (January 2012)

Volume 19 (2011): Issue 4 (December 2011)

Volume 19 (2011): Issue 3 (September 2011)

Volume 19 (2011): Issue 2 (June 2011)

Volume 19 (2011): Issue 1 (March 2011)

Volume 18 (2010): Issue 4 (December 2010)

Volume 18 (2010): Issue 3 (September 2010)

Volume 18 (2010): Issue 2 (June 2010)

Volume 18 (2010): Issue 1 (March 2010)

Volume 17 (2009): Issue 4 (December 2009)

Volume 17 (2009): Issue 3 (September 2009)

Volume 17 (2009): Issue 2 (June 2009)

Volume 17 (2009): Issue 1 (March 2009)

Volume 16 (2008): Issue 4 (December 2008)

Volume 16 (2008): Issue 3 (September 2008)

Volume 16 (2008): Issue 2 (June 2008)

Volume 16 (2008): Issue 1 (March 2008)

Volume 15 (2007): Issue 4 (December 2007)

Volume 15 (2007): Issue 3 (September 2007)

Volume 15 (2007): Issue 2 (June 2007)

Volume 15 (2007): Issue 1 (March 2007)

Volume 14 (2006): Issue 4 (December 2006)

Volume 14 (2006): Issue 3 (September 2006)

Volume 14 (2006): Issue 2 (June 2006)

Volume 14 (2006): Issue 1 (March 2006)

Journal Details
Format
Journal
eISSN
1898-9934
ISSN
1426-2630
First Published
09 Jun 2008
Publication timeframe
4 times per year
Languages
English

Search

Volume 25 (2017): Issue 2 (July 2017)

Journal Details
Format
Journal
eISSN
1898-9934
ISSN
1426-2630
First Published
09 Jun 2008
Publication timeframe
4 times per year
Languages
English

Search

8 Articles
Open Access

Vieta’s Formula about the Sum of Roots of Polynomials

Published Online: 23 Sep 2017
Page range: 87 - 92

Abstract

Summary

In the article we formalized in the Mizar system [2] the Vieta formula about the sum of roots of a polynomial anxn + an−1xn−1 + ··· + a1x + a0 defined over an algebraically closed field. The formula says that x1+x2++xn1+xn=an1an$x_1 + x_2 + \cdots + x_{n - 1} + x_n = - {{a_{n - 1} } \over {a_n }}$ , where x1, x2,…, xn are (not necessarily distinct) roots of the polynomial [12]. In the article the sum is denoted by SumRoots.

Keywords

  • roots of polynomials
  • Vieta’s formula

MSC 2010

  • 12E05
  • 03B35
Open Access

Basic Formal Properties of Triangular Norms and Conorms

Published Online: 23 Sep 2017
Page range: 93 - 100

Abstract

Summary

In the article we present in the Mizar system [1], [8] the catalogue of triangular norms and conorms, used especially in the theory of fuzzy sets [13]. The name triangular emphasizes the fact that in the framework of probabilistic metric spaces they generalize triangle inequality [2].

After defining corresponding Mizar mode using four attributes, we introduced the following t-norms:

minimum t-norm minnorm (Def. 6),

product t-norm prodnorm (Def. 8),

Łukasiewicz t-norm Lukasiewicz_norm (Def. 10),

drastic t-norm drastic_norm (Def. 11),

nilpotent minimum nilmin_norm (Def. 12),

Hamacher product Hamacher_norm (Def. 13),

and corresponding t-conorms:

maximum t-conorm maxnorm (Def. 7),

probabilistic sum probsum_conorm (Def. 9),

bounded sum BoundedSum_conorm (Def. 19),

drastic t-conorm drastic_conorm (Def. 14),

nilpotent maximum nilmax_conorm (Def. 18),

Hamacher t-conorm Hamacher_conorm (Def. 17).

Their basic properties and duality are shown; we also proved the predicate of the ordering of norms [10], [9]. It was proven formally that drastic-norm is the pointwise smallest t-norm and minnorm is the pointwise largest t-norm (maxnorm is the pointwise smallest t-conorm and drastic-conorm is the pointwise largest t-conorm).

This work is a continuation of the development of fuzzy sets in Mizar [6] started in [11] and [3]; it could be used to give a variety of more general operations on fuzzy sets. Our formalization is much closer to the set theory used within the Mizar Mathematical Library than the development of rough sets [4], the approach which was chosen allows however for merging both theories [5], [7].

Keywords

  • fuzzy set
  • triangular norm
  • triangular conorm
  • fuzzy logic

MSC 2010

  • 03E72
  • 94D05
  • 03B35
Open Access

Introduction to Stopping Time in Stochastic Finance Theory

Published Online: 23 Sep 2017
Page range: 101 - 105

Abstract

Summary

We start with the definition of stopping time according to [4], 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 [6], 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 ([7], p.372) and can be used together with stochastic processes ([4], 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}=∅ & {w, where w is Element of Ω: ST.w=1}={1,2} & {w, where w is Element of Ω: ST.w=2}={3,4} and

ST is a stopping time.

We use a function Filt as Filtration of {0,1,2}, Σ where Filt(0)=Ωnow, Filt(1)=Ωfut1 and Filt(2)=Ωfut2. From a., b. and c. we know that:

d. {w, where w is Element of Ω: ST.w=0} in Ωnow and

{w, where w is Element of Ω: ST.w=1} in Ωfut1 and

{w, where w is Element of Ω: ST.w=2} in Ωfut2.

The sets in d. are events, which occur at the time points 0(=now), 1(=tomorrow) or 2(=the day after tomorrow), see also [7], 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 [5].

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 f2(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 f3(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 f3(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 [7], p.372).

Keywords

  • stopping time
  • stochastic process

MSC 2010

  • 60G40
  • 03B35
Open Access

Pascal’s Theorem in Real Projective Plane

Published Online: 23 Sep 2017
Page range: 107 - 119

Abstract

Summary

In this article we check, with the Mizar system [2], Pascal’s theorem in the real projective plane (in projective geometry Pascal’s theorem is also known as the Hexagrammum Mysticum Theorem)1. Pappus’ theorem is a special case of a degenerate conic of two lines.

For proving Pascal’s theorem, we use the techniques developed in the section “Projective Proofs of Pappus’ Theorem” in the chapter “Pappus’ Theorem: Nine proofs and three variations” [11]. We also follow some ideas from Harrison’s work. With HOL Light, he has the proof of Pascal’s theorem2. For a lemma, we use PROVER93 and OTT2MIZ by Josef Urban4 [12, 6, 7]. We note, that we don’t use Skolem/Herbrand functions (see “Skolemization” in [1]).

Keywords

  • Pascal’s theorem
  • real projective plane
  • Grassman-Plücker relation

MSC 2010

  • 51E15
  • 51N15
  • 03B35
Open Access

About Quotient Orders and Ordering Sequences

Published Online: 23 Sep 2017
Page range: 121 - 139

Abstract

Summary

In preparation for the formalization in Mizar [4] of lotteries as given in [14], this article closes some gaps in the Mizar Mathematical Library (MML) regarding relational structures. The quotient order is introduced by the equivalence relation identifying two elements x, y of a preorder as equivalent if xy and yx. This concept is known (see e.g. chapter 5 of [19]) and was first introduced into the MML in [13] and that work is incorporated here. Furthermore given a set A, partition D of A and a finite-support function f : A → ℝ, a function Σf : D → ℝ, Σf (X)= ∑xXf(x) can be defined as some kind of natural “restriction” from f to D. The first main result of this article can then be formulated as: xAf(x)=XDΣf(X)(=XDxXf(x))$$\sum\limits_{x \in A} {f(x)} = \sum\limits_{X \in D} {\Sigma _f (X)\left( { = \sum\limits_{X \in D} {\sum\limits_{x \in X} {f(x)} } } \right)} $$

After that (weakly) ascending/descending finite sequences (based on [3]) are introduced, in analogous notation to their infinite counterparts introduced in [18] and [13].

The second main result is that any finite subset of any transitive connected relational structure can be sorted as a ascending or descending finite sequence, thus generalizing the results from [16], where finite sequence of real numbers were sorted.

The third main result of the article is that any weakly ascending/weakly descending finite sequence on elements of a preorder induces a weakly ascending/weakly descending finite sequence on the projection of these elements into the quotient order. Furthermore, weakly ascending finite sequences can be interpreted as directed walks in a directed graph, when the set of edges is described by ordered pairs of vertices, which is quite common (see e.g. [10]).

Additionally, some auxiliary theorems are provided, e.g. two schemes to find the smallest or the largest element in a finite subset of a connected transitive relational structure with a given property and a lemma I found rather useful: Given two finite one-to-one sequences s, t on a set X, such that rng t ⊆ rng s, and a function f : X → ℝ such that f is zero for every x ∈ rng s \ rng t, we have ∑ f o s = ∑ f o t.

Keywords

  • quotient order
  • ordered finite sequences

MSC 2010

  • 06A05
  • 03B35
Open Access

Basel Problem – Preliminaries

Published Online: 23 Sep 2017
Page range: 141 - 147

Abstract

Summary

In the article we formalize in the Mizar system [4] preliminary facts needed to prove the Basel problem [7, 1]. Facts that are independent from the notion of structure are included here.

Keywords

  • Basel problem

MSC 2010

  • 11M06
  • 03B35
Open Access

Basel Problem

Published Online: 23 Sep 2017
Page range: 149 - 155

Abstract

Summary

A rigorous elementary proof of the Basel problem [6, 1] n=11n2=π26$$\sum\nolimits_{n = 1}^\infty {{1 \over {n^2 }} = {{\pi ^2 } \over 6}} $$ is formalized in the Mizar system [3]. This theorem is item #14 from the “Formalizing 100 Theorems” list maintained by Freek Wiedijk at http://www.cs.ru.nl/F.Wiedijk/100/.

Keywords

  • Basel problem

MSC 2010

  • 11M06
  • 03B35
Open Access

Dual Lattice of ℤ-module Lattice

Published Online: 23 Sep 2017
Page range: 157 - 169

Abstract

Summary

In this article, we formalize in Mizar [5] the definition of dual lattice and their properties. We formally prove that a set of all dual vectors in a rational lattice has the construction of a lattice. We show that a dual basis can be calculated by elements of an inverse of the Gram Matrix. We also formalize a summation of inner products and their properties. Lattice of ℤ-module is necessary for lattice problems, LLL(Lenstra, Lenstra and Lovász) base reduction algorithm and cryptographic systems with lattice [20], [10] and [19].

Keywords

  • ℤ-lattice
  • dual lattice of ℤ-lattice
  • dual basis of ℤ-lattice

MSC 2010

  • 15A03
  • 15A09
  • 03B35
8 Articles
Open Access

Vieta’s Formula about the Sum of Roots of Polynomials

Published Online: 23 Sep 2017
Page range: 87 - 92

Abstract

Summary

In the article we formalized in the Mizar system [2] the Vieta formula about the sum of roots of a polynomial anxn + an−1xn−1 + ··· + a1x + a0 defined over an algebraically closed field. The formula says that x1+x2++xn1+xn=an1an$x_1 + x_2 + \cdots + x_{n - 1} + x_n = - {{a_{n - 1} } \over {a_n }}$ , where x1, x2,…, xn are (not necessarily distinct) roots of the polynomial [12]. In the article the sum is denoted by SumRoots.

Keywords

  • roots of polynomials
  • Vieta’s formula

MSC 2010

  • 12E05
  • 03B35
Open Access

Basic Formal Properties of Triangular Norms and Conorms

Published Online: 23 Sep 2017
Page range: 93 - 100

Abstract

Summary

In the article we present in the Mizar system [1], [8] the catalogue of triangular norms and conorms, used especially in the theory of fuzzy sets [13]. The name triangular emphasizes the fact that in the framework of probabilistic metric spaces they generalize triangle inequality [2].

After defining corresponding Mizar mode using four attributes, we introduced the following t-norms:

minimum t-norm minnorm (Def. 6),

product t-norm prodnorm (Def. 8),

Łukasiewicz t-norm Lukasiewicz_norm (Def. 10),

drastic t-norm drastic_norm (Def. 11),

nilpotent minimum nilmin_norm (Def. 12),

Hamacher product Hamacher_norm (Def. 13),

and corresponding t-conorms:

maximum t-conorm maxnorm (Def. 7),

probabilistic sum probsum_conorm (Def. 9),

bounded sum BoundedSum_conorm (Def. 19),

drastic t-conorm drastic_conorm (Def. 14),

nilpotent maximum nilmax_conorm (Def. 18),

Hamacher t-conorm Hamacher_conorm (Def. 17).

Their basic properties and duality are shown; we also proved the predicate of the ordering of norms [10], [9]. It was proven formally that drastic-norm is the pointwise smallest t-norm and minnorm is the pointwise largest t-norm (maxnorm is the pointwise smallest t-conorm and drastic-conorm is the pointwise largest t-conorm).

This work is a continuation of the development of fuzzy sets in Mizar [6] started in [11] and [3]; it could be used to give a variety of more general operations on fuzzy sets. Our formalization is much closer to the set theory used within the Mizar Mathematical Library than the development of rough sets [4], the approach which was chosen allows however for merging both theories [5], [7].

Keywords

  • fuzzy set
  • triangular norm
  • triangular conorm
  • fuzzy logic

MSC 2010

  • 03E72
  • 94D05
  • 03B35
Open Access

Introduction to Stopping Time in Stochastic Finance Theory

Published Online: 23 Sep 2017
Page range: 101 - 105

Abstract

Summary

We start with the definition of stopping time according to [4], 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 [6], 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 ([7], p.372) and can be used together with stochastic processes ([4], 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}=∅ & {w, where w is Element of Ω: ST.w=1}={1,2} & {w, where w is Element of Ω: ST.w=2}={3,4} and

ST is a stopping time.

We use a function Filt as Filtration of {0,1,2}, Σ where Filt(0)=Ωnow, Filt(1)=Ωfut1 and Filt(2)=Ωfut2. From a., b. and c. we know that:

d. {w, where w is Element of Ω: ST.w=0} in Ωnow and

{w, where w is Element of Ω: ST.w=1} in Ωfut1 and

{w, where w is Element of Ω: ST.w=2} in Ωfut2.

The sets in d. are events, which occur at the time points 0(=now), 1(=tomorrow) or 2(=the day after tomorrow), see also [7], 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 [5].

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 f2(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 f3(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 f3(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 [7], p.372).

Keywords

  • stopping time
  • stochastic process

MSC 2010

  • 60G40
  • 03B35
Open Access

Pascal’s Theorem in Real Projective Plane

Published Online: 23 Sep 2017
Page range: 107 - 119

Abstract

Summary

In this article we check, with the Mizar system [2], Pascal’s theorem in the real projective plane (in projective geometry Pascal’s theorem is also known as the Hexagrammum Mysticum Theorem)1. Pappus’ theorem is a special case of a degenerate conic of two lines.

For proving Pascal’s theorem, we use the techniques developed in the section “Projective Proofs of Pappus’ Theorem” in the chapter “Pappus’ Theorem: Nine proofs and three variations” [11]. We also follow some ideas from Harrison’s work. With HOL Light, he has the proof of Pascal’s theorem2. For a lemma, we use PROVER93 and OTT2MIZ by Josef Urban4 [12, 6, 7]. We note, that we don’t use Skolem/Herbrand functions (see “Skolemization” in [1]).

Keywords

  • Pascal’s theorem
  • real projective plane
  • Grassman-Plücker relation

MSC 2010

  • 51E15
  • 51N15
  • 03B35
Open Access

About Quotient Orders and Ordering Sequences

Published Online: 23 Sep 2017
Page range: 121 - 139

Abstract

Summary

In preparation for the formalization in Mizar [4] of lotteries as given in [14], this article closes some gaps in the Mizar Mathematical Library (MML) regarding relational structures. The quotient order is introduced by the equivalence relation identifying two elements x, y of a preorder as equivalent if xy and yx. This concept is known (see e.g. chapter 5 of [19]) and was first introduced into the MML in [13] and that work is incorporated here. Furthermore given a set A, partition D of A and a finite-support function f : A → ℝ, a function Σf : D → ℝ, Σf (X)= ∑xXf(x) can be defined as some kind of natural “restriction” from f to D. The first main result of this article can then be formulated as: xAf(x)=XDΣf(X)(=XDxXf(x))$$\sum\limits_{x \in A} {f(x)} = \sum\limits_{X \in D} {\Sigma _f (X)\left( { = \sum\limits_{X \in D} {\sum\limits_{x \in X} {f(x)} } } \right)} $$

After that (weakly) ascending/descending finite sequences (based on [3]) are introduced, in analogous notation to their infinite counterparts introduced in [18] and [13].

The second main result is that any finite subset of any transitive connected relational structure can be sorted as a ascending or descending finite sequence, thus generalizing the results from [16], where finite sequence of real numbers were sorted.

The third main result of the article is that any weakly ascending/weakly descending finite sequence on elements of a preorder induces a weakly ascending/weakly descending finite sequence on the projection of these elements into the quotient order. Furthermore, weakly ascending finite sequences can be interpreted as directed walks in a directed graph, when the set of edges is described by ordered pairs of vertices, which is quite common (see e.g. [10]).

Additionally, some auxiliary theorems are provided, e.g. two schemes to find the smallest or the largest element in a finite subset of a connected transitive relational structure with a given property and a lemma I found rather useful: Given two finite one-to-one sequences s, t on a set X, such that rng t ⊆ rng s, and a function f : X → ℝ such that f is zero for every x ∈ rng s \ rng t, we have ∑ f o s = ∑ f o t.

Keywords

  • quotient order
  • ordered finite sequences

MSC 2010

  • 06A05
  • 03B35
Open Access

Basel Problem – Preliminaries

Published Online: 23 Sep 2017
Page range: 141 - 147

Abstract

Summary

In the article we formalize in the Mizar system [4] preliminary facts needed to prove the Basel problem [7, 1]. Facts that are independent from the notion of structure are included here.

Keywords

  • Basel problem

MSC 2010

  • 11M06
  • 03B35
Open Access

Basel Problem

Published Online: 23 Sep 2017
Page range: 149 - 155

Abstract

Summary

A rigorous elementary proof of the Basel problem [6, 1] n=11n2=π26$$\sum\nolimits_{n = 1}^\infty {{1 \over {n^2 }} = {{\pi ^2 } \over 6}} $$ is formalized in the Mizar system [3]. This theorem is item #14 from the “Formalizing 100 Theorems” list maintained by Freek Wiedijk at http://www.cs.ru.nl/F.Wiedijk/100/.

Keywords

  • Basel problem

MSC 2010

  • 11M06
  • 03B35
Open Access

Dual Lattice of ℤ-module Lattice

Published Online: 23 Sep 2017
Page range: 157 - 169

Abstract

Summary

In this article, we formalize in Mizar [5] the definition of dual lattice and their properties. We formally prove that a set of all dual vectors in a rational lattice has the construction of a lattice. We show that a dual basis can be calculated by elements of an inverse of the Gram Matrix. We also formalize a summation of inner products and their properties. Lattice of ℤ-module is necessary for lattice problems, LLL(Lenstra, Lenstra and Lovász) base reduction algorithm and cryptographic systems with lattice [20], [10] and [19].

Keywords

  • ℤ-lattice
  • dual lattice of ℤ-lattice
  • dual basis of ℤ-lattice

MSC 2010

  • 15A03
  • 15A09
  • 03B35

Plan your remote conference with Sciendo