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

#### Search

#### Abstract

The article concerns about formalizing multivariable formal power series and polynomials [

1. translation between

2. formalization of a bag-based formal power series in multivariable case over a commutative ring denoted by

3. formalization of a polynomial ring in one variable by restricting one variable case denoted by

4. formalization of a ring isomorphism to the existing polynomial ring in one variable given by sequence:

#### Keywords

- bag
- formal power series
- polynomial ring

#### MSC

- 13F25
- 13B25
- 68V20

#### Abstract

This article generalizes the differential method on intervals, using the Mizar system [

Therefore, in this paper, based on these results, although it is limited to real one-variable functions, we formalize the differentiation on arbitrary intervals and summarize them as various basic propositions. In particular, the chain rule [

#### Keywords

- differentiation on closed interval
- chain rule

#### MSC

- 26A06
- 68V20

Open Access

#### Elementary Number Theory Problems. Part VII

Page range: 23 - 29

#### Abstract

In this paper problems 48, 80, 87, 89, and 124 from [

#### Keywords

- number theory
- divisibility
- primes

#### MSC

- 11A41
- 03B35
- 68V20

#### Abstract

In this article sets of certain subgraphs of a graph are formalized in the Mizar system [

#### Keywords

- graph enumeration
- spanning tree

#### MSC

- 05C05
- 05C30
- 68V20

Open Access

#### On the Formalization of Gram-Schmidt Process for Orthonormalizing a Set of Vectors

Page range: 53 - 57

#### Abstract

In this article, we formalize the Gram-Schmidt process in the Mizar system [

#### Keywords

- Gram-Schmidt process
- orthonormal basis
- linear algebra

#### MSC

- 65F25
- 94A11
- 97H60
- 68V20

Open Access

#### Isosceles Triangular and Isosceles Trapezoidal Membership Functions Using Centroid Method

Page range: 59 - 66

#### Abstract

Since isosceles triangular and trapezoidal membership functions [

We proved the agreement of the same function expressed with different parameters and formalized those centroids with parameters. In addition, various properties of membership functions on intervals where the endpoints of the domain are fixed and on general intervals are formalized in Mizar [

#### Keywords

- defuzzification
- centroid method
- isosceles triangular function
- isosceles trapezoidal function

#### MSC

- 03E72
- 93C42
- 94D05
- 68V20

#### Abstract

A classical algebraic geometry is study of zero points of system of multivariate polynomials [3], [7] and those zero points would be corresponding to points, lines, curves, surfaces in an affine space. In this article we give some basic definition of the area of affine algebraic geometry such as algebraic set, ideal of set of points, and those properties according to [4] in the Mizar system[5], [2].

We treat an affine space as the ^{n }

This formalization aims at providing basic notions of the field which enable to formalize geometric objects such as algebraic curves which is used e.g. in coding theory [11] as well as further formalization of the fields [8] in the Mizar system, including the theory of polynomials [6].

#### Keywords

- affine algebraic set
- multivariate polynomial

#### MSC

- 14-01
- 14H50
- 68V20

#### Abstract

In this article regular graphs, both directed and undirected, are formalized in the Mizar system [7], [2], based on the formalization of graphs as described in [10]. The handshaking lemma is also proven.

#### Keywords

- regular graphs

#### MSC

- 05C07
- 68V20

Open Access

#### Elementary Number Theory Problems. Part VIII

Page range: 87 - 100

#### Abstract

In this paper problems 25, 86, 88, 105, 111, 137–142, and 184–185 from [12] are formalized, using the Mizar formalism [3], [1], [4]. This is a continuation of the work from [5], [6], and [2] as suggested in [8]. The automatization of selected lemmas from [11] proven in this paper as proposed in [9] could be an interesting future work.

#### Keywords

- number theory
- divisibility
- primes
- factorization

#### MSC

- 11A41
- 03B35
- 68V20

Open Access

#### Internal Direct Products and the Universal Property of Direct Product Groups

Page range: 101 - 120

#### Abstract

This is a “quality of life” article concerning product groups, using the Mizar system [2], [4]. Like a Sonata, this article consists of three movements.

The first act, the slowest of the three, builds the infrastructure necessary for the rest of the article. We prove group homomorphisms map arbitrary finite products to arbitrary finite products, introduce a notion of “group yielding” families, as well as families of homomorphisms. We close the first act with defining the inclusion morphism of a subgroup into its parent group, and the projection morphism of a product group onto one of its factors.

The second act introduces the universal property of products and its consequences as found in, e.g., Kurosh [7]. Specifically, for the product of an arbitrary family of groups, we prove the center of a product group is the product of centers. More exciting, we prove for a product of a finite family groups, the commutator subgroup of the product is the product of commutator subgroups, but this is because in general: the direct sum of commutator subgroups is the subgroup of the commutator subgroup of the product group, and the commutator subgroup of the product is a subgroup of the product of derived subgroups. We conclude this act by proving a few theorems concerning the image and kernel of morphisms between product groups, as found in Hungerford [5], as well as quotients of product groups.

The third act introduces the notion of an internal direct product. Isaacs [6] points out (paraphrasing with Mizar terminology) that the internal direct product is a predicate but the external direct product is a [Mizar] functor. To our delight, we find the bulk of the “recognition theorem” (as stated by Dummit and Foote [3], Aschbacher [1], and Robinson [11]) are already formalized in the heroic work of Nakasho, Okazaki, Yamazaki, and Shimada [9], [8]. We generalize the notion of an internal product to a set of subgroups, proving it is equivalent to the internal product of a family of subgroups [10].

#### Keywords

- direct product of groups

#### MSC

- 20E22
- 68V20

#### Abstract

In this article we continue the formalization of field theory in Mizar [_{1}, . . . _{n}_{i}

#### Keywords

- normal extension
- fixing monomorphisms

#### MSC

- 12F05
- 68V20

#### Abstract

In this paper, we introduce indefinite integrals [

In the first section, we summarize the basic theorems on continuity and derivativity (for interesting survey of formalizations of real analysis in another proof-assistants like ACL2 [

#### Keywords

- antiderivative
- integration by substitution

#### MSC

- 26A06
- 68V20