Journal & Issues

Volume 30 (2022): Issue 3 (October 2022)

Volume 30 (2022): Issue 2 (July 2022)

Volume 30 (2022): Issue 1 (April 2022)

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
First Published
09 Jun 2008
Publication timeframe
4 times per year
Languages
English

Search

Volume 30 (2022): Issue 2 (July 2022)

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

Search

5 Articles
Open Access

Characteristic Subgroups

Published Online: 24 Dec 2022
Page range: 79 - 91

Abstract

Summary

We formalize in Mizar [1], [2] the notion of characteristic subgroups using the definition found in Dummit and Foote [3], as subgroups invariant under automorphisms from its parent group. Along the way, we formalize notions of Automorphism and results concerning centralizers. Much of what we formalize may be found sprinkled throughout the literature, in particular Gorenstein [4] and Isaacs [5]. We show all our favorite subgroups turn out to be characteristic: the center, the derived subgroup, the commutator subgroup generated by characteristic subgroups, and the intersection of all subgroups satisfying a generic group property.

Keywords

  • group theory
  • inner automorphisms
  • characteristic subgroups

MSC

  • 20E07
  • 20E15
  • 68V20
Open Access

Transformation Tools for Real Linear Spaces

Published Online: 24 Dec 2022
Page range: 93 - 98

Abstract

Summary

This paper, using the Mizar system [1], [2], provides useful tools for working with real linear spaces and real normed spaces. These include the identification of a real number set with a one-dimensional real normed space, the relationships between real linear spaces and real Euclidean spaces, the transformation from a real linear space to a real vector space, and the properties of basis and dimensions of real linear spaces. We referred to [6], [10], [8], [9] in this formalization.

Keywords

  • real linear space
  • real normed space
  • real Euclidean space
  • real vector space

MSC

  • 46A19 46A35 68V20
Open Access

Introduction to Graph Colorings

Published Online: 24 Dec 2022
Page range: 99 - 124

Abstract

Summary

In this article vertex, edge and total colorings of graphs are formalized in the Mizar system [4] and [1], based on the formalization of graphs in [5].

Keywords

  • graph coloring
  • edge coloring
  • total coloring

MSC

  • 68V20
  • 05C15
Open Access

Definition of Centroid Method as Defuzzification

Published Online: 24 Dec 2022
Page range: 125 - 134

Abstract

Summary

In this study, using the Mizar system [1], [2], we reuse formalization e orts in fuzzy sets described in [5] and [6]. This time the centroid method which is one of the fuzzy inference processes is formulated [10]. It is the most popular of all defuzzied methods ([11], [13], [7]) – here, defuzzified crisp value is obtained from domain of membership function as weighted average [8]. Since the integral is used in centroid method, the integrability and bounded properties of membership functions are also mentioned to fill the formalization gaps present in the Mizar Mathematical Library, as in the case of another fuzzy operators [4]. In this paper, the properties of piecewise linear functions consisting of two straight lines are mainly described.

Keywords

  • defuzzification
  • centroid
  • piecewise linear function

MSC

  • 68V20
  • 93C42
Open Access

Elementary Number Theory Problems. Part III

Published Online: 24 Dec 2022
Page range: 135 - 158

Abstract

Summary

In this paper problems 11, 16, 19–24, 39, 44, 46, 74, 75, 77, 82, and 176 from [10] are formalized as described in [6], using the Mizar formalism [1], [2], [4]. Problems 11 and 16 from the book are formulated as several independent theorems. Problem 46 is formulated with a given example of required properties. Problem 77 is not formulated using triangles as in the book is.

Keywords

  • number theory
  • divisibility
  • primes

MSC

  • 11A41
  • 03B35
  • 68V20
5 Articles
Open Access

Characteristic Subgroups

Published Online: 24 Dec 2022
Page range: 79 - 91

Abstract

Summary

We formalize in Mizar [1], [2] the notion of characteristic subgroups using the definition found in Dummit and Foote [3], as subgroups invariant under automorphisms from its parent group. Along the way, we formalize notions of Automorphism and results concerning centralizers. Much of what we formalize may be found sprinkled throughout the literature, in particular Gorenstein [4] and Isaacs [5]. We show all our favorite subgroups turn out to be characteristic: the center, the derived subgroup, the commutator subgroup generated by characteristic subgroups, and the intersection of all subgroups satisfying a generic group property.

Keywords

  • group theory
  • inner automorphisms
  • characteristic subgroups

MSC

  • 20E07
  • 20E15
  • 68V20
Open Access

Transformation Tools for Real Linear Spaces

Published Online: 24 Dec 2022
Page range: 93 - 98

Abstract

Summary

This paper, using the Mizar system [1], [2], provides useful tools for working with real linear spaces and real normed spaces. These include the identification of a real number set with a one-dimensional real normed space, the relationships between real linear spaces and real Euclidean spaces, the transformation from a real linear space to a real vector space, and the properties of basis and dimensions of real linear spaces. We referred to [6], [10], [8], [9] in this formalization.

Keywords

  • real linear space
  • real normed space
  • real Euclidean space
  • real vector space

MSC

  • 46A19 46A35 68V20
Open Access

Introduction to Graph Colorings

Published Online: 24 Dec 2022
Page range: 99 - 124

Abstract

Summary

In this article vertex, edge and total colorings of graphs are formalized in the Mizar system [4] and [1], based on the formalization of graphs in [5].

Keywords

  • graph coloring
  • edge coloring
  • total coloring

MSC

  • 68V20
  • 05C15
Open Access

Definition of Centroid Method as Defuzzification

Published Online: 24 Dec 2022
Page range: 125 - 134

Abstract

Summary

In this study, using the Mizar system [1], [2], we reuse formalization e orts in fuzzy sets described in [5] and [6]. This time the centroid method which is one of the fuzzy inference processes is formulated [10]. It is the most popular of all defuzzied methods ([11], [13], [7]) – here, defuzzified crisp value is obtained from domain of membership function as weighted average [8]. Since the integral is used in centroid method, the integrability and bounded properties of membership functions are also mentioned to fill the formalization gaps present in the Mizar Mathematical Library, as in the case of another fuzzy operators [4]. In this paper, the properties of piecewise linear functions consisting of two straight lines are mainly described.

Keywords

  • defuzzification
  • centroid
  • piecewise linear function

MSC

  • 68V20
  • 93C42
Open Access

Elementary Number Theory Problems. Part III

Published Online: 24 Dec 2022
Page range: 135 - 158

Abstract

Summary

In this paper problems 11, 16, 19–24, 39, 44, 46, 74, 75, 77, 82, and 176 from [10] are formalized as described in [6], using the Mizar formalism [1], [2], [4]. Problems 11 and 16 from the book are formulated as several independent theorems. Problem 46 is formulated with a given example of required properties. Problem 77 is not formulated using triangles as in the book is.

Keywords

  • number theory
  • divisibility
  • primes

MSC

  • 11A41
  • 03B35
  • 68V20

Plan your remote conference with Sciendo