- Journal Details
- Format
- Journal
- eISSN
- 1898-9934
- ISSN
- 1426-2630
- First Published
- 09 Jun 2008
- Publication timeframe
- 4 times per year
- Languages
- English
Search
- Open Access
Coproducts in Categories without Uniqueness of cod and dom
Page range: 235 - 239
Abstract
The paper introduces coproducts in categories without uniqueness of cod and dom. It is proven that set-theoretical disjoint union is the coproduct in the category Ens [9].
Keywords
- coproducts
- disjoined union
Abstract
Based on the Petri net definitions and theorems already formalized in the Mizar article [13], in this article we were able to formalize the definition of cell Petri nets. It is based on [12]. Colored Petri net has already been defined in [11]. In addition, the conditions of the firing rule and the colored set to this definition, that defines the cell Petri nets are further extended to CPNT.i further. The synthesis of two Petri nets was introduced in [11] and in this work the definition is extended to produce the synthesis of a family of colored Petri nets. Specifically, the extension to a CPNT family is performed by specifying how to link the outbound transitions of each colored Petri net to the place elements of other nets to form a neighborhood relationship. Finally, the activation of colored Petri nets was formalized.
Keywords
- Petri net
- system modelling
- Open Access
Isometric Differentiable Functions on Real Normed Space
Page range: 249 - 260
Abstract
In this article, we formalize isometric differentiable functions on real normed space [17], and their properties.
Keywords
- isometric differentiable function
- Open Access
Differential Equations on Functions from R into Real Banach Space
Page range: 261 - 272
Abstract
In this article, we describe the differential equations on functions from R into real Banach space. The descriptions are based on the article [20]. As preliminary to the proof of these theorems, we proved some properties of differentiable functions on real normed space. For the proof we referred to descriptions and theorems in the article [21] and the article [32]. And applying the theorems of Riemann integral introduced in the article [22], we proved the ordinary differential equations on real Banach space. We referred to the methods of proof in [30].
Keywords
- formalization of differential equations
Abstract
In this article, we formalize a free Z-module and its property. In particular, we formalize the vector space of rational field corresponding to a free Z-module and prove formally that submodules of a free Z-module are free. Z-module is necassary for lattice problems - LLL (Lenstra, Lenstra and Lov´asz) base reduction algorithm and cryptographic systems with lattice [20]. Some theorems in this article are described by translating theorems in [11] into theorems of Z-module, however their proofs are different.
Keywords
- free Z-module
- submodule of free Z-module