MML Query (home page)

Mizar project
page generated with MMLQT (MML Query Transformation) tool
Mizar home, download
files: abstr, articles,
bin, doc, emacs gabs, fmbibs, gabs (more) semantic MML
Megrez
MML Query (beta)

Template maker
Environment explanation
Mizar TWiki
MML Query server
Megrez services
Journals:
   FM: MetaPRESS, server, proof-read, regeneration
   MM&A (preparation)
Syntax: xml, html
Downloads
Mizar syntax, xml, txt
MML 5.57.1355
- most important facts (other collection) MML links Monographs
Conference MKM2004
Workshop 30 years of Mizar
dydaktyka (e-learning)
Mizar Mathematical Library (version 5.57.1355) includes 1357 articles written by 263 authors and 62163 theorems, 12840 definitions, 883 schemes, 15367 registrations, 9464 symbols. (more statistics, other versions)
New:      monograph: TG Set Theory      authors by # of important facts      environment explanation
decode
MML links:

Latest 30 articles (the query: list of article ordered by historical order reversed select 0-29)
  1. hilb10_5: Formalization of the MRDP Theorem in the Mizar System by Karol Pak (submitted May 27, 2019)
    21 theorems, 4 definitions, 2 schemes, 9 registrations, authors:Karol Pak, abstract, semantically linked, FM , full article, gab.

  2. hilb10_4: Diophantine Sets -- Preliminaries by Karol Pak (submitted May 27, 2019)
    39 theorems, 1 definition, no schemes, 8 registrations, authors:Karol Pak, abstract, semantically linked, FM , full article, gab.

  3. nomin_6: Partial Correctness of a Power Algorithm by Adrian Jaszczak (submitted May 27, 2019)
    12 theorems, 13 definitions, no schemes, 2 registrations, authors:Adrian Jaszczak, abstract, semantically linked, FM , full article, gab.

  4. nomin_5: Partial Correctness of a Factorial Algorithm by Adrian Jaszczak, Artur Kornilowicz (submitted May 27, 2019)
    14 theorems, 20 definitions, no schemes, 2 registrations, authors:Adrian Jaszczak. Artur Kornilowicz, abstract, semantically linked, FM , full article, gab.

  5. field_2: On Monomorphisms and Subfields by Christoph Schwarzweller (submitted May 27, 2019)
    19 theorems, 8 definitions, no schemes, 5 registrations, authors:Christoph Schwarzweller, abstract, semantically linked, FM , full article, gab.

  6. ndiff_9: Implicit Function Theorem -- Part II by Kazuhisa Nakasho, Yasunari Shidama (submitted May 27, 2019)
    21 theorems, no definitions, no schemes, no registrations, authors:Kazuhisa Nakasho. Yasunari Shidama, abstract, semantically linked, FM , full article, gab.

  7. lopban13: Invertible Operators on Banach Spaces by Kazuhisa Nakasho (submitted May 27, 2019)
    31 theorems, 3 definitions, no schemes, no registrations, authors:Kazuhisa Nakasho, abstract, semantically linked, FM , full article, gab.

  8. lopban12: Isomorphisms from the Space of Multilinear Operators by Kazuhisa Nakasho (submitted May 27, 2019)
    16 theorems, 1 definition, no schemes, 5 registrations, authors:Kazuhisa Nakasho, abstract, semantically linked, FM , full article, gab.

  9. field_1: On Roots of Polynomials over K[X]/<p> by Christoph Schwarzweller (submitted March 28, 2019)
    45 theorems, 6 definitions, no schemes, 13 registrations, authors:Christoph Schwarzweller, abstract, semantically linked, FM , full article, gab.

  10. ntalgo_2: Maximum Number of Steps Taken by Modular Exponentiation and Euclidean Algorithm by Hiroyuki Okazaki, Koich Nagao, Yuichi Futa (submitted March 11, 2019)
    22 theorems, 2 definitions, no schemes, no registrations, authors:Yuichi Futa. Koich Nagao. Hiroyuki Okazaki, abstract, semantically linked, FM , full article, gab.

  11. gtarski4: Tarski Geometry Axioms. Part IV -- Right angle by Roland Coghetto, Adam Grabowski (submitted March 11, 2019)
    48 theorems, 9 definitions, no schemes, no registrations, authors:Roland Coghetto. Adam Grabowski, abstract, semantically linked, FM , full article, gab.

  12. mesfun13: Fubini's Theorem by Noboru Endou (submitted March 11, 2019)
    33 theorems, 2 definitions, no schemes, 1 registration, authors:Noboru Endou, abstract, semantically linked, FM , full article, gab.

  13. lopban11: Continuity of Multilinear Operator on Normed Linear Spaces by Kazuhisa Nakasho, Yasunari Shidama (submitted February 27, 2019)
    14 theorems, no definitions, no schemes, 1 registration, authors:Kazuhisa Nakasho. Yasunari Shidama, abstract, semantically linked, FM , full article, gab.

  14. anproj10: Cross-ratio in Real Vector Space by Roland Coghetto (submitted February 27, 2019)
    77 theorems, 30 definitions, no schemes, 6 registrations, authors:Roland Coghetto, abstract, semantically linked, FM , full article, gab.

  15. lopban10: Multilinear Operator and Its Basic Properties by Kazuhisa Nakasho (submitted February 27, 2019)
    52 theorems, 16 definitions, no schemes, 20 registrations, authors:Kazuhisa Nakasho, abstract, semantically linked, FM , full article, gab.

  16. pdiffeq1: A Simple Example for Linear Partial Differential Equations and Its Solution Using the Method of Separation of Variables by Sora Otsuki, Pauline N. Kawamoto, Hiroshi Yamazaki (submitted February 27, 2019)
    23 theorems, no definitions, no schemes, 2 registrations, authors:Pauline N Kawamoto. Sora Otsuki. Hiroshi Yamazaki, abstract, semantically linked, FM , full article, gab.

  17. lopban_9: Bilinear Operators on Normed Linear Spaces by Kazuhisa Nakasho (submitted February 27, 2019)
    27 theorems, 9 definitions, no schemes, 18 registrations, authors:Kazuhisa Nakasho, abstract, semantically linked, FM , full article, gab.

  18. rvsum_4: Concatenation of Finite Sequences by Rafal Ziobro (submitted February 27, 2019)
    68 theorems, 14 definitions, no schemes, 91 registrations, authors:Rafal Ziobro, abstract, semantically linked, FM , full article, gab.

  19. topzari1: Zariski Topology by Yasushige Watase (submitted October 16, 2018)
    39 theorems, 16 definitions, no schemes, 15 registrations, authors:Yasushige Watase, abstract, semantically linked, FM , full article, gab.

  20. fuzimpl2: Fundamental Properties of Fuzzy Implications by Adam Grabowski (submitted September 29, 2018)
    17 theorems, 4 definitions, no schemes, 17 registrations, authors:Adam Grabowski, abstract, semantically linked, FM , full article, gab.

  21. music_s1: Pythagorean Tuning: Pentatonic and Heptatonic Scale by Roland Coghetto (submitted September 29, 2018)
    118 theorems, 103 definitions, no schemes, 17 registrations, authors:Roland Coghetto, abstract, semantically linked, FM , full article, gab.

  22. lopban_8: Continuity of Bounded Linear Operators on Normed Linear Spaces by Kazuhisa Nakasho, Yuichi Futa, Yasunari Shidama (submitted September 29, 2018)
    13 theorems, 3 definitions, no schemes, 3 registrations, authors:Yuichi Futa. Kazuhisa Nakasho. Yasunari Shidama, abstract, semantically linked, FM , full article, gab.

  23. binari_6: Binary Representation of Natural Numbers by Hiroyuki Okazaki (submitted September 29, 2018)
    41 theorems, 10 definitions, no schemes, 2 registrations, authors:Hiroyuki Okazaki, abstract, semantically linked, FM , full article, gab.

  24. tops_5: Some Remarks about Product Spaces by Sebastian Koch (submitted September 29, 2018)
    82 theorems, 5 definitions, no schemes, 20 registrations, authors:Sebastian Koch, abstract, semantically linked, FM , full article, gab.

  25. finseq_9: Arithmetic Operations on Short Finite Sequences by Rafal Ziobro (submitted September 29, 2018)
    51 theorems, 3 definitions, no schemes, 121 registrations, authors:Rafal Ziobro, abstract, semantically linked, FM , full article, gab.

  26. robbins5: On Two Alternative Axiomatizations of Lattices by McKenzie and Sholander by Adam Grabowski, Damian Sawicki (submitted June 29, 2018)
    15 theorems, 6 definitions, no schemes, 6 registrations, authors:Adam Grabowski. Damian Sawicki, abstract, semantically linked, FM , full article, gab.

  27. roughs_5: Formalizing Two Generalized Approximation Operators by Adam Grabowski, Michal Sielwiesiuk (submitted June 29, 2018)
    53 theorems, 7 definitions, no schemes, 7 registrations, authors:Adam Grabowski. Michal Sielwiesiuk, abstract, semantically linked, FM , full article, gab.

  28. hilb10_3: Basic Diophantine Relations by Marcin Acewicz, Karol Pak (submitted June 29, 2018)
    24 theorems, no definitions, 5 schemes, 1 registration, authors:Marcin Acewicz. Karol Pak, abstract, semantically linked, FM , full article, gab.

  29. nomin_4: Partial correctness of GCD algorithm by Ievgen Ivanov, Artur Kornilowicz, Mykola Nikitchenko (submitted June 29, 2018)
    28 theorems, 28 definitions, 3 schemes, 5 registrations, authors:Ievgen Ivanov. Artur Kornilowicz. Mykola Nikitchenko, abstract, semantically linked, FM , full article, gab.

  30. nomin_3: An inference system of an extension of Floyd-Hoare logic for partial predicates by Ievgen Ivanov, Artur Kornilowicz, Mykola Nikitchenko (submitted June 29, 2018)
    32 theorems, 4 definitions, no schemes, 1 registration, authors:Ievgen Ivanov. Artur Kornilowicz. Mykola Nikitchenko, abstract, semantically linked, FM , full article, gab.


Full list in reversed historical order (start querying) and lexical order of MML Id, titles, authors.
  1. version 5.57.1355
  2. version 5.45.1305 [differences]
  3. version 5.33.1254 [differences]
  4. version 5.25.1220 [differences]
[Compare two versions]
Grzegorz Bancerek: bancerek (at) mizar.org