<abstract xmlns="http://www.w3.org/1999/xhtml">
<bold>Summary</bold>. In this article we prove, using Mizar [2], [1], the Pappus’s hexagon theorem in the real projective plane: “Given one set of collinear points <italic>A, B, C</italic>, and another set of collinear points <italic>a, b, c</italic>, then the intersection points <italic>X, Y, Z</italic> of line pairs <italic>Ab</italic> and <italic>aB, Ac</italic> and <italic>aC, Bc</italic> and <italic>bC</italic> are collinear”<fn id="j_forma-2021-0007_fn_2" symbol="2"><ext-link ext-link-type="uri" xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="https://en.wikipedia.org/wiki/Pappus’s_hexagon_theorem">https://en.wikipedia.org/wiki/Pappus’s_hexagon_theorem</ext-link></fn>.
More precisely, we prove that the structure <monospace>ProjectiveSpace TOP-REAL3</monospace> [10] (where <monospace>TOP-REAL3</monospace> is a metric space defined in [5]) satisfies the Pappus’s axiom defined in [11] by Wojciech Leończuk and Krzysztof Prażmowski. Eugeniusz Kusak and Wojciech Leończuk formalized the Hessenberg theorem early in the MML [9]. 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” [12]. Secondly, Pascal’s theorem [4] is used.
In both cases, to prove some lemmas, we use <monospace>Prover9</monospace><fn id="j_forma-2021-0007_fn_3" symbol="3"><ext-link ext-link-type="uri" xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="https://www.cs.unm.edu/~mccune/prover9/">https://www.cs.unm.edu/~mccune/prover9/</ext-link></fn>, the successor of the <monospace>Otter</monospace> prover and <monospace>ott2miz</monospace> by Josef Urban<fn id="j_forma-2021-0007_fn_4" symbol="4">See its homepage <ext-link ext-link-type="uri" xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="https://github.com/JUrban/ott2miz">https://github.com/JUrban/ott2miz</ext-link></fn> [13], [8], [7].
In <monospace>Coq</monospace>, the Pappus’s theorem is proved as the application of Grassmann-Cayley algebra [6] and more recently in Tarski’s geometry [3].
</abstract>

Pappus’s Hexagon Theorem in Real Projective Plane

<abstract xmlns="http://www.w3.org/1999/xhtml">
<bold>Summary</bold>. 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 [15], dealing also with alternative versions of classical axiomatizations. Some of the results were proven in the Mizar [1], [2] system with the help of Prover9 [14] proof assistant.
</abstract>

On Weakly Associative Lattices and Near Lattices

<abstract xmlns="http://www.w3.org/1999/xhtml">
<bold>Summary</bold>. In this article we formalize the Ascoli-Arzelà theorem [5], [6], [8] in Mizar [1], [2]. First, we gave definitions of equicontinuousness and equiboundedness of a set of continuous functions [12], [7], [3], [9]. Next, we formalized the Ascoli-Arzelà theorem using those definitions, and proved this theorem.
</abstract>

Nagano Prefectural Institute of Technology Nagano

Ibaraki University Faculty of Engineering Hitachi

Ascoli-Arzelà Theorem

<abstract xmlns="http://www.w3.org/1999/xhtml">
<bold>Summary</bold>. We formalize in the Mizar System [3], [4], definitions and basic propositions about primary ideals of a commutative ring along with Chapter 4 of [1] and Chapter III of [8]. 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 [1] and compiled as preliminaries in the first half of the article.
</abstract>

On Primary Ideals. Part I

<abstract xmlns="http://www.w3.org/1999/xhtml">
<bold>Summary</bold>. 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 [7]. 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 [12]. 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 [9], [10], [4]. 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 [3] formalizations of triangular and trapezoidal function composed of two straight lines, minimum function and maximum functions are proposed. We prove, using the Mizar [2], [1] formalism, some properties of membership functions such as continuity and periodicity [13], [8].
</abstract>

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

AHEAD OF PRINT

Volume 31 (2023): Issue 1 (September 2023)

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 (December 2012)

Volume 20 (2012): Issue 2 (December 2012)

Volume 20 (2012): Issue 1 (January 2012)

Volume 19 (2011): Issue 4 (January 2011)

Volume 19 (2011): Issue 3 (January 2011)

Volume 19 (2011): Issue 2 (January 2011)

Volume 19 (2011): Issue 1 (March 2011)

Volume 18 (2010): Issue 4 (January 2010)

Volume 18 (2010): Issue 3 (September 2010)

Volume 18 (2010): Issue 2 (January 2010)

Volume 18 (2010): Issue 1 (January 2010)

Volume 17 (2009): Issue 4 (January 2009)

Volume 17 (2009): Issue 3 (January 2009)

Volume 17 (2009): Issue 2 (June 2009)

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

Volume 16 (2008): Issue 4 (January 2008)

Volume 16 (2008): Issue 3 (January 2008)

Volume 16 (2008): Issue 2 (January 2008)

Volume 16 (2008): Issue 1 (January 2008)

Volume 15 (2007): Issue 4 (January 2007)

Volume 15 (2007): Issue 3 (September 2007)

Volume 15 (2007): Issue 2 (January 2007)

Volume 15 (2007): Issue 1 (January 2007)

Volume 14 (2006): Issue 4 (December 2006)

Volume 14 (2006): Issue 3 (January 2006)

Volume 14 (2006): Issue 2 (January 2006)

Volume 14 (2006): Issue 1 (January 2006)

Formalized Mathematics

  Pioneering Journal in the field of formalized and mechanically checked mathematics. Excellent articles on latest research in formal methods and computer-checked mathematics. Full-length original research articles in English. Archival issues available at the journal's home page fm.mizar.org/.   To build a uniform and extensible computer-checked repository of mathematical knowledge.  Reconstruction of mathematics based on mechanization of mathematical reasoning.  To check a wide range of mathematical theorems using a computer in an automatic fashion.  General mathematics: especially topology, lattice theory, functional analysis.  Applications: computer-aided verification of software and hardware, computer-aided teaching of mathematics.   Why subscribe and read   Pioneering source of high quality research in formalized and mechanically checked mathematics.  The oldest journal in the field, a medium for the publication of research reporting pioneering findings of broad mathematical significance that are likely to advance the direction and thinking of the field.  Long-term experience in publishing original articles on mechanizing mathematics and various aspects of automated reasoning, since 1990.   Why submit   Fair and constructive peer review by international experts in the field (three referees are designated for the assessment of each manuscript) - double-blind review process.  New publishing technology: articles automatically translated from a formal language into English and automatically typeset, available in both forms - electronic and printed.  Articles abstracted by online indexing services and databases.   Rejection Rate   59% of submitted articles.  The rejection percentage is described in detail in the following paper, pp.239-240: dx.doi.org/10.1007/978-3-540-73086-6_20 Archiving  Sciendo archives the contents of this journal in Portico - digital long-term preservation service of scholarly books, journals and collections.  Plagiarism Policy  The editorial board is participating in a growing community of Similarity Check System's users in order to ensure that the content published is original and trustworthy. Similarity Check is a medium that allows for comprehensive manuscripts screening, aimed to eliminate plagiarism and provide a high standard and quality peer-review process. Back Issues fm.mizar.org/   Other Files  Addenda 2008Formalized Mathematics Bibliography File.Formalized Mathematics External Bibliography File.  "In years: 2016-2017, the English version of Formalized Mathematics was financed under agreements 548/P-DUN/2016 and 548/1/P-DUN/2016 with the funds from the Polish Minister of Science and Higher Education for the dissemination of science." 