- Journal Details
- Format
- Journal
- eISSN
- 1898-9934
- First Published
- 09 Jun 2008
- Publication timeframe
- 4 times per year
- Languages
- English
Search
Abstract
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
Page range: 93 - 98
Abstract
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
Abstract
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
Page range: 125 - 134
Abstract
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
Page range: 135 - 158
Abstract
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