1. Home
  2. Formalized Mathematics
  3. Volume 17 (2009): Issue 1 (March 2009)

Issues

Journal & Issues

Formalized Mathematics's Cover Image
Formalized Mathematics

Volume 30 (2022): Issue 4 (December 2022)

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

Search

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

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

Search

5 Articles
Open Access

The Real Vector Spaces of Finite Sequences are Finite Dimensional

Yatsuka Nakamura,
Yatsuka Nakamura,
Artur Korniłowicz,
Artur Korniłowicz,
Nagato Oya and
Nagato Oya and
Yasunari Shidama
Yasunari Shidama
Published Online: 20 Mar 2009
Page range: 1 - 9

Abstract

The Real Vector Spaces of Finite Sequences are Finite Dimensional

In this paper we show the finite dimensionality of real linear spaces with their carriers equal Rn. We also give the standard basis of such spaces. For the set Rn we introduce the concepts of linear manifold subsets and orthogonal subsets. The cardinality of orthonormal basis of discussed spaces is proved to equal n.

MML identifier: EUCLID 7, version: 7.11.01 4.117.1046

Open Access

Several Integrability Formulas of Some Functions, Orthogonal Polynomials and Norm Functions

Bo Li,
Bo Li,
Yanping Zhuang,
Yanping Zhuang,
Bing Xie and
Bing Xie and
Pan Wang
Pan Wang
Published Online: 20 Mar 2009
Page range: 11 - 21

Abstract

Several Integrability Formulas of Some Functions, Orthogonal Polynomials and Norm Functions

In this article, we give several integrability formulas of some functions including the trigonometric function and the index function [3]. We also give the definitions of the orthogonal polynomial and norm function, and some of their important properties [19].

MML identifier: INTEGRA9, version: 7.11.01 4.117.1046

Open Access

Several Integrability Formulas of Special Functions. Part II

Bo Li,
Bo Li,
Yanping Zhuang,
Yanping Zhuang,
Yanhong Men and
Yanhong Men and
Xiquan Liang
Xiquan Liang
Published Online: 20 Mar 2009
Page range: 23 - 35

Abstract

Several Integrability Formulas of Special Functions. Part II

In this article, we give several differentiation and integrability formulas of special and composite functions including the trigonometric function, the hyperbolic function and the polynomial function [3].

MML identifier: INTEGR11, version: 7.11.01 4.117.1046

Open Access

Cell Petri Net Concepts

Mitsuru Jitsukawa,
Mitsuru Jitsukawa,
Pauline Kawamoto,
Pauline Kawamoto,
Yasunari Shidama and
Yasunari Shidama and
Yatsuka Nakamura
Yatsuka Nakamura
Published Online: 20 Mar 2009
Page range: 37 - 42

Abstract

Cell Petri Net Concepts

Based on the Petri net definitions and theorems already formalized in [8], with this article, we developed the concept of "Cell Petri Nets". It is based on [9]. In a cell Petri net we introduce the notions of colors and colored states of a Petri net, connecting mappings for linking two Petri nets, firing rules for transitions, and the synthesis of two or more Petri nets.

MML identifier: PETRI 2, version: 7.11.01 4.117.1046

Open Access

Arithmetic Operations on Functions from Sets into Functional Sets

Artur Korniłowicz
Artur Korniłowicz
Published Online: 20 Mar 2009
Page range: 43 - 60

Abstract

Arithmetic Operations on Functions from Sets into Functional Sets

In this paper we introduce sets containing number-valued functions. Different arithmetic operations on maps between any set and such functional sets are later defined.

MML identifier: VALUED 2, version: 7.11.01 4.117.1046

5 Articles
Open Access

The Real Vector Spaces of Finite Sequences are Finite Dimensional

Yatsuka Nakamura,
Yatsuka Nakamura,
Artur Korniłowicz,
Artur Korniłowicz,
Nagato Oya and
Nagato Oya and
Yasunari Shidama
Yasunari Shidama
Published Online: 20 Mar 2009
Page range: 1 - 9

Abstract

The Real Vector Spaces of Finite Sequences are Finite Dimensional

In this paper we show the finite dimensionality of real linear spaces with their carriers equal Rn. We also give the standard basis of such spaces. For the set Rn we introduce the concepts of linear manifold subsets and orthogonal subsets. The cardinality of orthonormal basis of discussed spaces is proved to equal n.

MML identifier: EUCLID 7, version: 7.11.01 4.117.1046

Open Access

Several Integrability Formulas of Some Functions, Orthogonal Polynomials and Norm Functions

Bo Li,
Bo Li,
Yanping Zhuang,
Yanping Zhuang,
Bing Xie and
Bing Xie and
Pan Wang
Pan Wang
Published Online: 20 Mar 2009
Page range: 11 - 21

Abstract

Several Integrability Formulas of Some Functions, Orthogonal Polynomials and Norm Functions

In this article, we give several integrability formulas of some functions including the trigonometric function and the index function [3]. We also give the definitions of the orthogonal polynomial and norm function, and some of their important properties [19].

MML identifier: INTEGRA9, version: 7.11.01 4.117.1046

Open Access

Several Integrability Formulas of Special Functions. Part II

Bo Li,
Bo Li,
Yanping Zhuang,
Yanping Zhuang,
Yanhong Men and
Yanhong Men and
Xiquan Liang
Xiquan Liang
Published Online: 20 Mar 2009
Page range: 23 - 35

Abstract

Several Integrability Formulas of Special Functions. Part II

In this article, we give several differentiation and integrability formulas of special and composite functions including the trigonometric function, the hyperbolic function and the polynomial function [3].

MML identifier: INTEGR11, version: 7.11.01 4.117.1046

Open Access

Cell Petri Net Concepts

Mitsuru Jitsukawa,
Mitsuru Jitsukawa,
Pauline Kawamoto,
Pauline Kawamoto,
Yasunari Shidama and
Yasunari Shidama and
Yatsuka Nakamura
Yatsuka Nakamura
Published Online: 20 Mar 2009
Page range: 37 - 42

Abstract

Cell Petri Net Concepts

Based on the Petri net definitions and theorems already formalized in [8], with this article, we developed the concept of "Cell Petri Nets". It is based on [9]. In a cell Petri net we introduce the notions of colors and colored states of a Petri net, connecting mappings for linking two Petri nets, firing rules for transitions, and the synthesis of two or more Petri nets.

MML identifier: PETRI 2, version: 7.11.01 4.117.1046

Open Access

Arithmetic Operations on Functions from Sets into Functional Sets

Artur Korniłowicz
Artur Korniłowicz
Published Online: 20 Mar 2009
Page range: 43 - 60

Abstract

Arithmetic Operations on Functions from Sets into Functional Sets

In this paper we introduce sets containing number-valued functions. Different arithmetic operations on maps between any set and such functional sets are later defined.

MML identifier: VALUED 2, version: 7.11.01 4.117.1046