- 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

#### Isomorphism Theorem on Vector Spaces over a Ring

Page range: 171 - 178

#### Abstract

In this article, we formalize in the Mizar system [

#### Keywords

- isomorphism theorem
- vector space

#### MSC 2010

- 15A03
- 15A04
- 03B35

#### Abstract

In this article, we formalize in the Mizar system [

In Sec.2, we proved some lemmas for the proof of F. Riesz theorem. In Sec.3, we proved F. Riesz theorem, about the dual space of the space of continuous functions on closed interval subset of real numbers, finally. We applied Hahn-Banach theorem (36) in [

#### Keywords

- F. Riesz theorem
- dual spaces
- continuous functions

#### MSC 2010

- 46E15
- 46B10
- 03B35

Open Access

#### On Roots of Polynomials and Algebraically Closed Fields

Page range: 185 - 195

#### Abstract

In this article we further extend the algebraic theory of polynomial rings in Mizar [

#### Keywords

- commutative algebra
- polynomials
- algebraic closed fields

#### MSC 2010

- 13A05
- 13B25
- 03B35

#### Abstract

In this article we formalize several basic theorems that correspond to Pell’s equation. We focus on two aspects: that the Pell’s equation ^{2} − ^{2} = 1 has infinitely many solutions in positive integers for a given

“Solutions to Pell’s Equation” are listed as item

#### Keywords

- Pell’s equation
- Diophantine equation
- Hilbert’s 10th problem

#### MSC 2010

- 11D45
- 03B35

Open Access

#### Simple-Named Complex-Valued Nominative Data – Definition and Basic Operations

Page range: 205 - 216

#### Abstract

In this paper we give a formal definition of the notion of nominative data with simple names and complex values [

The notion of nominative data plays an important role in the composition-nominative approach to program formalization [

The composition-nominative approach considers mathematical models of computer software and data on various levels of abstraction and generality and provides mathematical tools for reasoning about their properties. In particular, nominative data are mathematical models of data which are stored and processed in computer systems. The composition-nominative approach considers different types [

In the composition-nominative approach computer programs which process data are modeled as partial functions which map nominative data from the carrier of a given data algebra (input data) to nominative data (output data). Such functions are also called

For functions over nominative data a special computability called abstract computability is introduces and complete classes of computable functions are specified [

For reasoning about properties of programs modeled as binominative functions a Floyd-Hoare style logic [

Besides modeling data processed by programs, nominative data can be also applied to modeling data processed by signal processing systems in the context of the mathematical systems theory [

#### Keywords

- program semantics
- software verification
- nominative data

#### MSC 2010

- 68Q60
- 03B70
- 03B35

#### Abstract

Some authors have formalized the integral in the Mizar Mathematical Library (MML). The first article in a series on the Darboux/Riemann integral was written by Noboru Endou and Artur Korniłowicz: [

A presentation of definitions of integrals in other proof assistants or proof checkers (ACL2, COQ, Isabelle/HOL, HOL4, HOL Light, PVS, ProofPower) may be found in [

Using the Mizar system [

In the last section, we verified that a real-valued bounded integrable (in sense Darboux/Riemann [

Note that, in accordance with the possibilities of the MML [

#### Keywords

- Gauge integral
- Henstock-Kurzweil integral
- generalized Riemann integral

#### MSC 2010

- 26A39
- 26A42
- 03B35

#### Abstract

In this article, we formalize in the Mizar system [

#### Keywords

- integration of non positive function

#### MSC 2010

- 28A25
- 03B35

Open Access

#### Formal Introduction to Fuzzy Implications

Page range: 241 - 248

#### Abstract

In the article we present in the Mizar system the catalogue of nine basic fuzzy implications, used especially in the theory of fuzzy sets. This work is a continuation of the development of fuzzy sets in Mizar; it could be used to give a variety of more general operations, and also it could be a good starting point towards the formalization of fuzzy logic (together with t-norms and t-conorms, formalized previously).

#### Keywords

- fuzzy implication
- fuzzy set
- fuzzy logic

#### MSC 2010

- 03B52
- 68T37
- 03B35