Mechanized Mathematics and Its Applications, Works in Progress (MMA-WiP) ISSN 2434-5458 (Online)

Mechanized Mathematics and Its Applications, Works in Progress (MMA-WiP) publishes papers that report the interpretation and/or application of a wide variety of mathematical concepts contained in articles verified by the Mizar proof-checking system (for information on Mizar, see http://mizar.org/). The papers are meant to complement Mizar articles by providing expositions of the usefulness of the results, insights, broad developments, or specific applications of the propositions.

Issue 2024, Volume 6

  • Yasushige Watase, On Primary Decomposition. MMA-WiP (2024), vol.6, no.1, pp.1-19. (online 2024.4.2) [PDF]
  • Takashi Mitsuishi, Properties of Symmetrical Piecewise Linear Functions Composed by Absolute Value Function. MMA-WiP (2024), vol.6, no.2, pp.1-8. (online 2024.4.2) [PDF]

Issue 2023, Volume 5

  • Yasushige Watase, On Identification of Rings. MMA-WiP (2023), vol.5, no.3, pp.1-8. (online 2023.7.3)[PDF]
  • Takashi Mitsuishi, Centroids of Isosceles Triangular and Isosceles Trapezoidal Membership Functions. MMA-WiP (2023), vol.5, no.1, pp.1-13. (online 2023.4.2)[PDF]
  • Kazuhisa Nakasho, Yasunari Shidama, On The Formalizations for Implicit Function Theorem with Higher Derivatives of Vector Valued Functions. MMA-WiP (2023), vol.5, no.2, pp.1-15. (online 2023.4.2)[PDF]
  • Yasushige Watase, On Identification of Rings. MMA-WiP (2023), vol.5, no.3, pp.1-8. (online 2023.7.3)[PDF]

Issue 2022, Volume 4

  • Roland Coghetto, Highschool (Secondary School) Trigonometry: Some Exercices with Mizar. MMA-WiP (2022), vol.4, no.1, pp.1-17 (online 2022.3.11)[PDF]
  • Yasunari Shidama, Kazuhisa Nakasho, On The Formalizations for Higher Derivatives of Vector Valued Functions. MMA-WiP (2022), vol.4, no.2, pp.1-16 (online 2022.6.10)[PDF][Erratum]
  • Yasushige Watase, On the Formalizations of Algebraic Geometry. MMA-WiP (2022), vol.4, no.3, pp.1-14 (online 2022.6.23)[PDF]
  • Keiichi Miyajima, Hiroshi Yamazaki, On The Formalization of Ascoli–Arzelà’s Theorem. MMA-WiP (2022), vol.4, no.4, pp.1-15 (online 2022.6.25)[PDF]
  • Takashi Mitsuishi, On the Formalizations of Definition for Centroid Method as Defuzzification. MMA-WiP (2022), vol.4, no.5, pp.1-12 (online 2022.6.7)[PDF]

Issue 2021, Volume 3

  • Yatsuka Nakamura, On n-dimensional Real Spaces and n-dimensional Complex Spaces I. MMA-WiP (2021), vol.3, no.1, pp.1-10. (online 2021.10.5)[PDF] [HTML] [article]
  • Takashi Mitsuishi, On the Formalizations of Definition for Set of Membership Functions and Several Types of Membership Functions. MMA-WiP (2021), vol.3, no.2, pp.1-16. (online 2021.10.5)[PDF]
  • Yasushige Watase, Derivation of Commutative Ring and its Application. MMA-WiP (2021), vol.3, no.3, pp.1-13. (online 2021.10.5)[PDF]
  • Hiroshi Yamazaki, Yasunari Shidama, On the Formalizations for Multilayer Perceptron. MMA-WiP (2021), vol.3, no.4, pp.1-12. (online 2021.10.5)[PDF]

Issue 2020, Volume 2

  • Yasunari Shidama, On the Formalizations for Functional Spaces of Continuous Functions. MMA-WiP (2020), vol.2, no.1, pp.1-16. (online 2020.11.30)[PDF]
  • Yasushige Watase, Properties of Modules over a Commutative Ring. MMA-WiP (2020), vol.2, no.2, pp.1-15. (online 2020.11.30)[PDF]
  • Kazuhisa Nakasho, Proposal of Information-theoretical Framework for Measuring Theorem Similarity. MMA-WiP (2020), vol.2, no.3, pp.1-8. (online 2020.11.30)[PDF]

Issue 2019, Volume 1

  • Kazuhisa Nakasho, Development of Mizar Lexer and Parser Working without Environment Part (Work in Progress). MMA-WiP (2019), vol.1, no.1, pp.1-7 (online 2019.9.27) [PDF]
  • Yasunari Shidama, On the Formalizations of Riemann-Stieltjes Integral. MMA-WiP (2019), vol.1, no.2, pp.1-13 (online 2019.9.27) [PDF]
  • Yasushige Watase, Zariski Topology. MMA-WiP (2019), vol.1, no.3, pp.1-12 (online 2019.9.27) [PDF]
  • Yasushige Watase, Localization of Commutative Rings. MMA-WiP (2019), vol.1, no.4, pp.1-11 (online 2019.9.27) [PDF]

 

Submission of Papers

Authors are invited to submit papers for review in LaTeX or MS-Word format (8 pages(min) — 16 pages(max), letter size) by e-mail to:

submission (at) mizar-jp.org

Papers must be written in Japanese or English, and include a list of references containing at least one Mizar article which serves as the basis of the paper for ‘Regular Paper’. A cover page should be provided to indicate the following information: paper category; title; authors and affiliations; address, and e-mail address of the corresponding author; a descriptive abstract of 200 words or less; and a maximum of five keywords describing the work. All submissions must be followed by canonical LaTeX/MS-Word paper style format (ZIP download).

Instructions for Authors

This PDF file is included submission guidelines and requirements of Mizar articles for the submission category; ‘Regular Paper’, ‘System Development Paper’, ‘Article’ and ‘Letter’ (Japanese text is here).

Correspondence

Correspondence (2019-): Mizar JAPAN; Shinshu University, Faculty of Engineering, Department of Electrical and Computer Engineering, c/o Katsumi Wasaki, Wakasato 4-17-1, Nagago, JAPAN 380-8553.

This journal is published online by Mizar JAPAN. Every paper is peer-reviewed and the editorial board reserves the right to edit papers.

Editorial Board

Katsumi Wasaki (Shinshu University)

Noboru Endou (National Institute of Technology, Gifu College)
Kazuhisa Nakasho (Yamaguchi University)

Ken’ichi Arai (Nagasaki Univerisity)
Hiroyuki Okazaki (Shinshu University)
Yasunari Shidama (Shinshu University, Professor Emeritus)
Yatsuka Nakamura (Shinshu University, Professor Emeritus)
Hiroshi Yamazaki (Nagano Prefectural Institute of Technology)
Takashi Mitsuishi (Nagano University)
Keiichi Miyajima (Ibaraki University)
Yasushige Watase (Suginami-ku, Tokyo)

 

 

 

 


 

Mechanized Mathematics and Its Applications (MMA) ISSN 1345-8272 (Print)

Mechanized Mathematics and Its Applications (MMA) publishes papers which report the interpretation and/or application of a wide variety of mathematical concepts contained in articles verified by the Mizar proof-checking system (for information on Mizar, see http://mizar.org/). The papers are meant to complement Mizar articles by providing expositions of the usefulness of the results, insights, broad developments, or specific applications of the propositions.

Released Volumes

  • Volume 1, 2000 [PDF]
  • Volume 2, 2002 [PDF]
  • Volume 3, 2004 [PDF]
  • Volume 4, 2005, “Special Issue on 30 Years of Mizar” [PDF]
  • Volume 5, Number 1, 2006 [PDF]
  • Volume 5, Number 2, 2006 [PDF]
  • Volume 6, 2007, “Special Issue on Jordan Curve Theorem” [PDF]
  • Volume 7, Number 1-2, 2008 [PDF]
  • Volume 8, 2010 [PDF]
  • Volume 9, Number 1-2, 2014 [PDF]

Submission of Papers

Authors are invited to submit papers for review in MS-Word format (V5.0 or later, 8 pages maximum, A4 size) by e-mail to:

pauline (at) cs.shinshu-u.ac.jp

Papers must be written in English and include a list of references containing at least one Mizar article which serves as the basis of the paper. A separate cover page should be provided to indicate the following information: title; authors and affiliations; address, e-mail and telephone/fax number of the primary author; a descriptive abstract of 200 words or less; and a maximum of five keywords describing the work. Adhere to the style of this journal as much as possible.

Correspondence

This journal is published annually by Mizar JAPAN. Every paper is reviewed and the editorial board reserves the right to edit papers.

Correspondence: Mizar JAPAN, Shinshu University, Faculty of Engineering, Department of Information Engineering, c/o Pauline N. Kawamoto, Nagano-ken Nagano-shi Wakasato 4-17-1, JAPAN 380-8553.