MML Query (home page)

Mizar project at Bialystok Technical University
page generated with MMLQT (MML Query Transformation) tool
Mizar home, download
unpacked files: abstr, bib, bin, doc, emacs gab's, mml
Mizar syntax, xml, txt
semantic MML (more), gabs (more)
Mizar TWiki
Megrez services
MML Query server
Journals: FM (server)
   MM&A (preparation)
Merak (UwB) server
Megrez
MML Query (beta)

Syntax: xml, html
Downloads, Template maker
MML 4.100.1011
- most important facts Statistics Monographs
Conference MKM2004
Workshop 30 years of Mizar
dydaktyka (e-learning)
Mizar Mathematical Library (version 4.100.1011) includes 1011 articles written by 207 authors and 46506 theorems, 8804 definitions, 756 schemes, 7925 registrations, 6489 symbols. (more statistics, other versions)

New:
Latest 30 articles (the query: list of article ordered by historical order reversed select 0-29)
  1. aofa_i00: Mizar Analysis of Algorithms: Algorithms over Integers by Grzegorz Bancerek (submitted March 18, 2008)
    67 theorem(s), 82 definition(s), 2 scheme(s), 9 registration(s), abstract, full article, gab, semantic presentation.
  2. mesfunc9: The Lebesgue Monotone Convergence Theorem by Noboru Endou, Keiko Narita, Yasunari Shidama (submitted March 18, 2008)
    52 theorem(s), 9 definition(s), 0 scheme(s), 1 registration(s), abstract, full article, gab, semantic presentation.
  3. sincos10: Inverse Trigonometric Functions Arcsec1, Arcsec2, Arccosec1 and Arccosec2 by Bing Xie, Xiquan Liang, Fuguo Ge (submitted March 18, 2008)
    132 theorem(s), 8 definition(s), 0 scheme(s), 12 registration(s), abstract, full article, gab, semantic presentation.
  4. sin_cos9: Inverse Trigonometric Functions Arctan and Arccot by Xiquan Liang, Bing Xie (submitted March 18, 2008)
    130 theorem(s), 4 definition(s), 0 scheme(s), 6 registration(s), abstract, full article, gab, semantic presentation.
  5. hfdiff_1: Several Higher Differentiation Formulas of Special Functions by Junjie Zhao, Xiquan Liang, Li Yan (submitted March 18, 2008)
    68 theorem(s), 0 definition(s), 0 scheme(s), 0 registration(s), abstract, full article, gab, semantic presentation.
  6. quatern2: Inner Products, Group, Ring of Quaternion Numbers by Fuguo Ge (submitted March 18, 2008)
    58 theorem(s), 13 definition(s), 0 scheme(s), 8 registration(s), abstract, full article, gab, semantic presentation.
  7. convex4: Convex Sets and Convex Combinations on Complex Linear Spaces by Hidenori Matsuzaki, Noboru Endou, Yasunari Shidama (submitted March 3, 2008)
    89 theorem(s), 26 definition(s), 0 scheme(s), 11 registration(s), abstract, full article, gab, semantic presentation.
  8. c0sp1: Banach Algebra of Bounded Functionals by Yasunari Shidama, Hikofumi Suzuki, Noboru Endou (submitted March 3, 2008)
    38 theorem(s), 18 definition(s), 0 scheme(s), 13 registration(s), abstract, full article, gab, semantic presentation.
  9. bciideal: Ideals of BCI-Algebras and Their Properties by Chenglong Wu, Yuzhong Ding (submitted March 3, 2008)
    57 theorem(s), 8 definition(s), 0 scheme(s), 2 registration(s), abstract, full article, gab, semantic presentation.
  10. scmnorm: Normal computers by Andrzej Trybulec (submitted March 3, 2008)
    0 theorem(s), 0 definition(s), 0 scheme(s), 2 registration(s), abstract, full article, gab, semantic presentation.
  11. int_7: Uniqueness of factoring an integer and multiplicative group $Z/pZ^*$ by Hiroyuki Okazaki, Yasunari Shidama (submitted January 31, 2008)
    31 theorem(s), 4 definition(s), 0 scheme(s), 2 registration(s), abstract, full article, gab, semantic presentation.
  12. euclid_6: Heron's Formula and Ptolemy's Theorem by Marco Riccardi (submitted January 10, 2008)
    52 theorem(s), 3 definition(s), 0 scheme(s), 0 registration(s), abstract, full article, gab, semantic presentation.
  13. helly: Helly property for subtrees by Jessica Enright, Piotr Rudnicki (submitted January 10, 2008)
    53 theorem(s), 4 definition(s), 0 scheme(s), 5 registration(s), abstract, full article, gab, semantic presentation.
  14. matrix15: Solutions of Linear Equations by Karol Pak (submitted December 18, 2007)
    76 theorem(s), 5 definition(s), 2 scheme(s), 1 registration(s), abstract, full article, gab, semantic presentation.
  15. gfacirc2: Stability of n-bit Generalized Full Adder Circuits (GFAs). Part II by Katsumi Wasaki (submitted December 18, 2007)
    28 theorem(s), 8 definition(s), 0 scheme(s), 2 registration(s), abstract, full article, gab, semantic presentation.
  16. valued_1: Properties of Number-valued Functions by Library Committee (submitted December 18, 2007)
    24 theorem(s), 12 definition(s), 0 scheme(s), 103 registration(s), abstract, full article, gab, semantic presentation.
  17. algstr_0: Basic Algebraic Structures by Library Committee (submitted December 8, 2007)
    0 theorem(s), 42 definition(s), 0 scheme(s), 78 registration(s), abstract, full article, gab, semantic presentation.
  18. bcialg_4: BCI-Algebras with Condition (S) and Their Properties by Tao Sun, Junjie Zhao, Xiquan Liang (submitted November 24, 2007)
    52 theorem(s), 15 definition(s), 0 scheme(s), 12 registration(s), abstract, full article, gab, semantic presentation.
  19. valued_0: Number-valued Functions by Library Committee (submitted November 22, 2007)
    12 theorem(s), 12 definition(s), 0 scheme(s), 110 registration(s), abstract, full article, gab, semantic presentation.
  20. mesfunc8: Egoroff's Theorem by Noboru Endou, Yasunari Shidama, Keiko Narita (submitted October 30, 2007)
    30 theorem(s), 10 definition(s), 0 scheme(s), 2 registration(s), abstract, full article, gab, semantic presentation.
  21. mesfunc7: The First Mean Value Theorem for Integrals by Keiko Narita, Noboru Endou, Yasunari Shidama (submitted October 30, 2007)
    26 theorem(s), 4 definition(s), 0 scheme(s), 8 registration(s), abstract, full article, gab, semantic presentation.
  22. diff_2: Difference and Difference Quotient -- Part II by Bo Li, Yanping Zhuang, Xiquan Liang (submitted October 25, 2007)
    72 theorem(s), 2 definition(s), 0 scheme(s), 0 registration(s), abstract, full article, gab, semantic presentation.
  23. compl_sp: Complete Spaces by Karol Pak (submitted October 12, 2007)
    44 theorem(s), 11 definition(s), 1 scheme(s), 16 registration(s), abstract, full article, gab, semantic presentation.
  24. flang_3: Regular Expression Quantifiers -- at least $m$ Occurrences by Michal Trybulec (submitted October 9, 2007)
    96 theorem(s), 2 definition(s), 0 scheme(s), 0 registration(s), abstract, full article, gab, semantic presentation.
  25. int_5: Gauss Lemma and Law of Quadratic Reciprocity by Li Yan, Xiquan Liang, Junjie Zhao (submitted October 9, 2007)
    51 theorem(s), 3 definition(s), 0 scheme(s), 2 registration(s), abstract, full article, gab, semantic presentation.
  26. lopban_5: Uniform Boundedness Principle by Hideki Sakurai, Hisayoshi Kunimune, Yasunari Shidama (submitted October 9, 2007)
    8 theorem(s), 2 definition(s), 0 scheme(s), 1 registration(s), abstract, full article, gab, semantic presentation.
  27. polyform: Euler's Polyhedron Formula by Jesse Alama (submitted October 9, 2007)
    92 theorem(s), 31 definition(s), 1 scheme(s), 4 registration(s), abstract, full article, gab, semantic presentation.
  28. bspace: The Vector Space of Subsets of a Set Based on Disjoint Union by Jesse Alama (submitted October 9, 2007)
    44 theorem(s), 11 definition(s), 1 scheme(s), 6 registration(s), abstract, full article, gab, semantic presentation.
  29. bcialg_3: Several Classes of BCK-algebras and Their Properties by Tao Sun, Dahai Hu, Xiquan Liang (submitted September 19, 2007)
    48 theorem(s), 12 definition(s), 0 scheme(s), 9 registration(s), abstract, full article, gab, semantic presentation.
  30. fdiff_10: Several Differentiation Formulas of Special Functions -- Part VI by Bo Li, Pan Wang (submitted September 19, 2007)
    46 theorem(s), 0 definition(s), 0 scheme(s), 0 registration(s), abstract, full article, gab, semantic presentation.

Full list in reversed historical order (start querying) and lexical order of MML Id, titles, authors.
  1. version 4.99.1005 [differences]
  2. version 4.97.1001 [differences]
  3. version 4.95.999 [differences]
  4. version 4.93.997 [differences]
  5. version 4.92.996 [differences]
  6. version 4.87.985 [differences]
  7. version 4.84.971 [differences]
  8. version 4.83.967 [differences]
  9. version 4.81.962 [differences]
  10. version 4.79.961 [differences]
  11. version 4.76.959 [differences]
  12. version 4.75.958 [differences]
  13. version 4.70.946 [differences]
  14. version 4.66.942 [differences]
  15. version 4.53.937 [differences]
  16. version 4.50.934 [differences]
  17. version 4.46.926 [differences]
  18. version 4.39.921 [differences]
  19. version 4.38.916 [differences]
  20. version 4.35.912 [differences]
  21. version 4.33.908 [differences]
  22. version 4.31.904 [differences]
  23. version 4.27.900 [differences]
  24. version 4.20.885 [differences]
  25. version 4.19.880 [differences]
  26. version 4.18.878 [differences]
  27. version 4.16.871 [differences]
  28. version 4.15.858 [differences]
  29. version 4.14.855 [differences]
  30. version 4.100.1011 [differences]
  31. version 4.10.851 [differences]
  32. version 4.09.842 [differences]
  33. version 4.04.834 [differences]
  34. version 4.03.825 [differences]
  35. version 3.65.806 [differences]
  36. version 3.63.801 [differences]
  37. version 3.54.781 [differences]
  38. version 3.46.767 [differences]
  39. version 3.42.755 [differences]
  40. version 3.36.725 [differences]
[Compare two versions]
Grzegorz Bancerek: bancerek@mizar.org