- 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

Vieta’s Formula about the Sum of Roots of Polynomials

Page range: 87 - 92

#### Abstract

In the article we formalized in the Mizar system [_{n}x^{n}_{n−}_{1}^{n−}^{1} + _{1}_{0} defined over an algebraically closed field. The formula says that
_{1}, _{2},…, _{n}

#### Keywords

- roots of polynomials
- Vieta’s formula

#### MSC 2010

- 12E05
- 03B35

- Open Access

Basic Formal Properties of Triangular Norms and Conorms

Page range: 93 - 100

#### Abstract

In the article we present in the Mizar system [

After defining corresponding Mizar mode using four attributes, we introduced the following t-norms:

minimum t-norm

product t-norm

Łukasiewicz t-norm

drastic t-norm

nilpotent minimum

Hamacher product

maximum t-conorm

probabilistic sum

bounded sum

drastic t-conorm

nilpotent maximum

Hamacher t-conorm

Their basic properties and duality are shown; we also proved the predicate of the ordering of norms [

This work is a continuation of the development of fuzzy sets in Mizar [

#### Keywords

- fuzzy set
- triangular norm
- triangular conorm
- fuzzy logic

#### MSC 2010

- 03E72
- 94D05
- 03B35

- Open Access

Introduction to Stopping Time in Stochastic Finance Theory

Page range: 101 - 105

#### Abstract

We start with the definition of stopping time according to [

a. ST(1)=1, ST(2)=1, ST(3)=2, ST(4)=2.

b. The set {0,1,2} consists of time points: 0=now,1=tomorrow,2=the day after tomorrow.

We can prove:

c. {w, where w is Element of Ω: ST.w=0}=∅ & {w, where w is Element of Ω: ST.w=1}={1,2} & {w, where w is Element of Ω: ST.w=2}={3,4} and

ST is a stopping time.

We use a function Filt as Filtration of {0,1,2}, Σ where Filt(0)=Ω_{now}_{fut}_{1} and Filt(2)=Ω_{fut}_{2}. From a., b. and c. we know that:

d. {w, where w is Element of Ω: ST.w=0} in Ω_{now}

{w, where w is Element of Ω: ST.w=1} in Ω_{fut}_{1} and

{w, where w is Element of Ω: ST.w=2} in Ω_{fut}_{2}.

The sets in d. are events, which occur at the time points 0(=now), 1(=tomorrow) or 2(=the day after tomorrow), see also [

As an interpretation for our installed functions consider the given adapted stochastic process in the article [

ST(1)=1 means, that the given element 1 in {1,2,3,4} is stopped in 1 (=tomorrow). That tells us, that we have to look at the value _{2}(1) which is equal to 80. The same argumentation can be applied for the element 2 in {1,2,3,4}.

ST(3)=2 means, that the given element 3 in {1,2,3,4} is stopped in 2 (=the day after tomorrow). That tells us, that we have to look at the value _{3}(3) which is equal to 100.

ST(4)=2 means, that the given element 4 in {1,2,3,4} is stopped in 2 (=the day after tomorrow). That tells us, that we have to look at the value _{3}(4) which is equal to 120.

In the real world, these functions can be used for questions like: when does the share price exceed a certain limit? (see [

#### Keywords

- stopping time
- stochastic process

#### MSC 2010

- 60G40
- 03B35

- Open Access

Pascal’s Theorem in Real Projective Plane

Page range: 107 - 119

#### Abstract

In this article we check, with the Mizar system [^{1}. Pappus’ theorem is a special case of a degenerate conic of two lines.

For proving Pascal’s theorem, we use the techniques developed in the section “Projective Proofs of Pappus’ Theorem” in the chapter “Pappus’ Theorem: Nine proofs and three variations” [^{2}. For a lemma, we use PROVER9^{3} and OTT2MIZ by Josef Urban^{4} [

#### Keywords

- Pascal’s theorem
- real projective plane
- Grassman-Plücker relation

#### MSC 2010

- 51E15
- 51N15
- 03B35

- Open Access

About Quotient Orders and Ordering Sequences

Page range: 121 - 139

#### Abstract

In preparation for the formalization in Mizar [_{f}_{f}_{x∈X}

After that (weakly) ascending/descending finite sequences (based on [

The second main result is that any finite subset of any transitive connected relational structure can be sorted as a ascending or descending finite sequence, thus generalizing the results from [

The third main result of the article is that any weakly ascending/weakly descending finite sequence on elements of a preorder induces a weakly ascending/weakly descending finite sequence on the projection of these elements into the quotient order. Furthermore, weakly ascending finite sequences can be interpreted as directed walks in a directed graph, when the set of edges is described by ordered pairs of vertices, which is quite common (see e.g. [

Additionally, some auxiliary theorems are provided, e.g. two schemes to find the smallest or the largest element in a finite subset of a connected transitive relational structure with a given property and a lemma I found rather useful: Given two finite one-to-one sequences

#### Keywords

- quotient order
- ordered finite sequences

#### MSC 2010

- 06A05
- 03B35

#### Abstract

In the article we formalize in the Mizar system [

#### Keywords

- Basel problem

#### MSC 2010

- 11M06
- 03B35

#### Abstract

A rigorous elementary proof of the Basel problem [6, 1]

#### Keywords

- Basel problem

#### MSC 2010

- 11M06
- 03B35

#### Abstract

In this article, we formalize in Mizar [

#### Keywords

- ℤ-lattice
- dual lattice of ℤ-lattice
- dual basis of ℤ-lattice

#### MSC 2010

- 15A03
- 15A09
- 03B35