# Volume 29 (2021): Issue 2 (July 2021)

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

5 Articles

Open Access

#### Pappus’s Hexagon Theorem in Real Projective Plane

Published Online: 30 Dec 2021
Page range: 69 - 76

#### Abstract

Summary. In this article we prove, using Mizar , , the Pappus’s hexagon theorem in the real projective plane: “Given one set of collinear points A, B, C, and another set of collinear points a, b, c, then the intersection points X, Y, Z of line pairs Ab and aB, Ac and aC, Bc and bC are collinear”

https://en.wikipedia.org/wiki/Pappus’s_hexagon_theorem

.

More precisely, we prove that the structure ProjectiveSpace TOP-REAL3  (where TOP-REAL3 is a metric space defined in ) satisfies the Pappus’s axiom defined in  by Wojciech Leończuk and Krzysztof Prażmowski. Eugeniusz Kusak and Wojciech Leończuk formalized the Hessenberg theorem early in the MML . With this result, the real projective plane is Desarguesian. For proving the Pappus’s theorem, two different proofs are given. First, we use the techniques developed in the section “Projective Proofs of Pappus’s Theorem” in the chapter “Pappos’s Theorem: Nine proofs and three variations” . Secondly, Pascal’s theorem  is used.

In both cases, to prove some lemmas, we use Prover9

https://www.cs.unm.edu/~mccune/prover9/

, the successor of the Otter prover and ott2miz by Josef Urban

See its homepage https://github.com/JUrban/ott2miz

, , .

In Coq, the Pappus’s theorem is proved as the application of Grassmann-Cayley algebra  and more recently in Tarski’s geometry .

#### Keywords

• Pappus’s Hexagon Theorem
• real projective plan
• Grassmann-Plücker relation
• Prover9

• 51N15
• 03B35
• 68V20
Open Access

#### On Weakly Associative Lattices and Near Lattices

Published Online: 30 Dec 2021
Page range: 77 - 85

#### Abstract

Summary. The main aim of this article is to introduce formally two generalizations of lattices, namely weakly associative lattices and near lattices, which can be obtained from the former by certain weakening of the usual well-known axioms. We show selected propositions devoted to weakly associative lattices and near lattices from Chapter 6 of , dealing also with alternative versions of classical axiomatizations. Some of the results were proven in the Mizar ,  system with the help of Prover9  proof assistant.

#### Keywords

• weakly associative lattice
• near lattice

• 68V20
• 06B05
• 06B75
Open Access

#### Ascoli-Arzelà Theorem

Published Online: 30 Dec 2021
Page range: 87 - 94

#### Abstract

Summary. In this article we formalize the Ascoli-Arzelà theorem , ,  in Mizar , . First, we gave definitions of equicontinuousness and equiboundedness of a set of continuous functions , , , . Next, we formalized the Ascoli-Arzelà theorem using those definitions, and proved this theorem.

#### Keywords

• Ascoli-Arzela’s theorem
• equicontinuousness of continuous functions
• equiboundedness of continuous functions

• 46B50
• 68V20
Open Access

#### On Primary Ideals. Part I

Published Online: 30 Dec 2021
Page range: 95 - 101

#### Abstract

Summary. We formalize in the Mizar System , , definitions and basic propositions about primary ideals of a commutative ring along with Chapter 4 of  and Chapter III of . Additionally other necessary basic ideal operations such as compatibilities taking radical and intersection of finite number of ideals are formalized as well in order to prove theorems relating primary ideals. These basic operations are mainly quoted from Chapter 1 of  and compiled as preliminaries in the first half of the article.

#### Keywords

• primary ideal
• prime ideal

• 13A70
• 16D70
• 68V20
Open Access

#### Some Properties of Membership Functions Composed of Triangle Functions and Piecewise Linear Functions

Published Online: 30 Dec 2021
Page range: 103 - 115

#### Abstract

Summary. IF-THEN rules in fuzzy inference is composed of multiple fuzzy sets (membership functions). IF-THEN rules can therefore be considered as a pair of membership functions . The evaluation function of fuzzy control is composite function with fuzzy approximate reasoning and is functional on the set of membership functions. We obtained continuity of the evaluation function and compactness of the set of membership functions . Therefore, we proved the existence of pair of membership functions, which maximizes (minimizes) evaluation function and is considered IF-THEN rules, in the set of membership functions by using extreme value theorem. The set of membership functions (fuzzy sets) is defined in this article to verifier our proofs before by Mizar , , . Membership functions composed of triangle function, piecewise linear function and Gaussian function used in practice are formalized using existing functions.

On the other hand, not only curve membership functions mentioned above but also membership functions composed of straight lines (piecewise linear function) like triangular and trapezoidal functions are formalized. Moreover, different from the definition in  formalizations of triangular and trapezoidal function composed of two straight lines, minimum function and maximum functions are proposed. We prove, using the Mizar ,  formalism, some properties of membership functions such as continuity and periodicity , .

#### Keywords

• membership function
• piecewise linear function

• 03E72
• 68V20