MMA-WiP Author Guidelines(1st Edition Authorized by the Editorial Board on September 28, 2019)(2nd Edition Authorized by the Editorial Board on September 23, 2021)

Journal name: Mechanized Mathematics and Its Applications, Works in Progress
Abbreviation: MMA-WiP

This instruction ensures authors entire flow of an article submission, editing rules and regarding
polices and regulations. The official text is in Japanese. English text is provided for the convenience of
the author.

Contents
1. Submission Guideline
2. Article Style and Format (LaTeX & Word)
3. Submission Procedure
4. Publication fee

1. Submission Guideline

1.1 Introduction
Concept:
It is the explicit goal of the journal to provides a forum for research in the Mathematical and Informatic
formal method based on the Mizar, a proof checker application, in an updated, timely manner. The
submission rule is the same principle as of the existing journal Mechanized Mathematics andApplications (MMA). Any article must be verified or related by the Mizar proof checking system.
For the sake of keeping the immediacy of sharing information, the following criteria are required forsubmitting articles where an article is meant, either Regular Paper, System Development Paper, Article
Paper, or Letter. A detailed explanation would appear in the next section.

Regular Paper, System Development Paper, and Article Paper:(1) Any Research Areas are in Scope of MMA-WiP as far as it relates to Mizar. Notion or theories
proposed in the article must be codified and verified by the Mizar proof checking system.

1(2) System Development Paper on developing application which is based on an idea appeared in existing
published Mizar articles is in scope. System Development Paper on developing Tools which is
support for generating theorems of Mizar articles is in scope as well.
(3) The review must be carried out in a shorter period under consideration of the rapid progress ofindustry technologies, and the publishing method is taken on an online basis to timely deliver.
(4) Authors manuscript and associated Mizar articles verified by a proof checker are stored in MMAWiP online (Article) repository that is open to the public in order to reuse coded theorems and toshare for anyone could access to the latest resource of the area. The repository is owned and operated
by mizar-jp.org.
(5) Those authors whose manuscript is regarded as accepted or being under the review process, arehighly encouraged to present his/her manuscripts in the annual Mizar symposium, it is frequently
held during the year-end period.
(6) It is encouraged for Authors to submit machine verified notions and theories that appeared in the
MMA-WiP manuscript to the Polish journal of Formalized Mathematics (FM).
(7) If the above submission to FM is accepted, then the coded part of the manuscript stored in MMAWiP online repository would be erased, simply because it is able to refer to the same article in MML
Library after FM would include it.

Letter:Scope and Contents of the research area are the same as regular paper. However, the Letter aims toprovide a forum among researchers in line with the following points (8)-(10).

(8) Sharing the latest research results of informatic or formal mathematical new idea or invented notion
which has been verified by Mizar.
(9) Discussion of an article already stored in the online repository.
(10) Journal intends to provide a forum where a proposal for an innovative idea, technical improvement,or presenting a problem regarding research topics.

1.2 Submission
The journal accepts Regular Papers, System Development Paper, Article Paper and Letters, as shownin the previous section.
All submitted manuscripts must be fulfilling the following requirements explained in the subsections
from 1.2.1 to 1.2.4 would be commonly applied to either Regular Paper, System Development Papers,
or Letter. Table 1 and 2 explain the specific requirements for each particular article case. It is emphasized,
prior to any requirements, the ethics of being a researcher and engineer must not be compromised.

21.2.1 Originality
・Proposed notions should not be derived from existing theorems in MML in a trivial manner.
・In the case of System Development Paper, even proposed system is combined known technics, and it
could be treated as new if the following criteria are met:a) The same combination has not been applied,b) The system itself is new, andc) New findings derived from the system.
・Comply copyrights policy and it is not allowed dual submitting, the author should not, in general,publish manuscripts essentially the same contents in multiple journals.

1.2.2 Significance・Journal expects the author’s contribution would have some significance to reinforce or widen the
research area.
・Impact or importance of articles would be measured potentially by estimating how much it is utilized
or referred to the MML libraries.
・Regarding to system-related research, authors emphasize the advantage of their proposed software
comparing existing similar systems by benchmark testing or by available technical data. In a case asystem is completely new, there is no existing system one could compare, necessarily justificationof its advantage is required.

1.2.3 Reliability
・Reliability of an article is guaranteed by the following manner, presented notions and ideas aretranslated to Mizar code and verified in the Mizar proof checking system.
・An article on a study of system development, it is not required to describe intermediate detailed test
result. It is fully the author’s responsibility to assure the reliabilities of their result. The followings
are to be considered prior to submit a manuscript:
・References are enumerated properly completed without any particular bias.
・Technical results are evaluated by appropriate comparison with the existing system, and its result is
concluded by appropriate reasoning.
・System Development article consists of three parts; theoretical presentation, computation experiment,
and evaluation of the result. Justifications of the result should be done by supporting test or backtesting. However, the idea itself is excellent, and rigorous support test may not be required.
・Conditions of test/experiment must be precisely described.

3

1.2.4 Comprehensive
・Author’s claim and its argument must be comprehensive based on structured and clear reasoning.
・As for System Development Report, it must include technical background and its Interpretation into
formal methods in order to reader could see the relation between the engineering aspect and formal
method.
・For Article Paper, only the contents of files that have passed the Mizar proof checker (****.miz,***.voc) will be published. Therefore, authors are requested to remove unnecessary citations andproof steps as much as possible in the environment and body sections using the utilities provided by
the Mizar support system.
(Please refer to the procedure described in http://mizar.org/library/submit.html)

Table.1 Criteria of Contents & Requirements for Regular Paper
Elements

Contents

Requirements (Regular Paper)
The submission rule is the same principle
as of the existing journal, Mechanized
Mathematics and Applications (MMA).

Any Research Areas is in Scope of
Scope

MMA-WiP as far as it relates to
Mizar

Any article must be verified by the Mizar
proof checking system. It is allowed topresent a system application based on
existing published Mizar articles orsupporting tools for the proof checker
Mizar. These articles are called “System
Development Paper.”
The proposed notion should not be derived
from existing theorems in MML in a trivial

The main result and contents of thesubmitted paper must be unpublished.
Originality

The proposed notion should not bederived from existing theorems in
MML in a trivial manner.

manner.

In

Development

the

case

Paper,

of

Systemeven

proposed

system is combined known technics, it
could be treated as new if the following
criteria are met; a) The same combination
has not been applied, b) System itself isnew, c) Deliverables from the systemprovide new results.

4

The impact or importance of articles would
be measured potentially by estimating how
much it is utilized or referred to the MML
JournalSignificance

expects

contribution

would

the

author’s libraries.

havesome In the case of System Development Paper,significance to reinforce or widen the there is no existing system one could
research area.

compareforjustificationofhis/herpresenting system, necessarily a reasoningof its advantage would be presented topersuade the audience effectively.
The reliability of an article isguaranteed by the following manner,
Reliability

presented notions and ideas aretranslated to Mizar code and verified
in the Mizar proof checking system.

In the case of System Development Paper,
results can be thought to be reliable if thefollowing information, which technologies
are combined, which kind of environmentand condition are deployed, are clearly
described.
In the case of System Development Paper,
it must include technical background andits Interpretation into formal methods inorder to reader could see the relation
between the engineering aspect and formal

The author’s claim and its argument
Comprehensive must be comprehensive based on
structured and clear reasoning.

method.
For Article Paper, only the contents of files
that have passed the Mizar proof checker(****.miz, ***.voc) will be published.
Therefore, authors are requested to remove
unnecessary citations and proof steps as
much as possible in the environment andbody sections using the utilities provided
by the Mizar support system.

5

Table.2 Criteria of Contents & Requirements for Letter(Scope and Contents are the same as Table.1)
Requirements (Letter)
LatestDecision Criteria

Research

Report(Take Discussion / Problem presentation

advantage of quick announcement)(Object to inspire readers awareness on
the problem)

Originality

Most important

Partially importantSignificance

Necessary

According to the above objective

Being verified by the Mizar proof
Reliability

checking system guarantees its
reliability.

Comprehensive

According to the scope/ Mizar proof
checker and MML libraries or develop
support tools. The problem should havegeneralities.

Claim and its argument must be comprehensive based on structured and clear
reasoning. The scope can be reduced from Regular Paper.

61.3 Definition of Public Publications
In this guideline, Public Publications mean those magazines or books which can be available at thedomestic or internal market and those journals which include refereed paper and issued by academic
societies or institutes. Authors are allowed to submit articles that have been appeared in other publishedmaterial rather than give a definition of the publication and deem to be no potential copyright violation
as a new article. However, the author should clarify the fact with a copy of its evidence. Those material
which has been appeared in a conference sponsored or co-sponsored by MMA-WiP are not necessary
to attach.

1.4 Copyright1.4.1 Copyright ownershipAll copyrights, whether inside or outside Japan (hereinafter including all rights provided for in
Articles 21 through 28 of the Copyright Law of Japan) for the papers submitted to the MMA-WiP shallin principle belong to the mizar-jp.org site as from the time when the manuscript is registered in MMAWiP online repository. By electrically submitting the manuscript to MMA-WiP, it is regarded that theauthor agrees on copyright policy stated in this Author Guidelines.
For the method of transferring copyright when electronic submission is not possible, the author
should contact the Society's Editorial Committee.

Rights of Authors:
Authors have other rights rather than transferred copyright.
(a) Authors have other rights, such as a patent.
(b) Authors may use their materials partially to compile their publication list.
(c) Authors may distribute copies of materials for non-commercial purposes, such as classroom
teaching.
(d) Authors shall comply with domestic copyright law.

1.4.2 Exception for Submission to other publication
Authors may not submit an article which is essentially same content as MMA-WiP has received toother academic societies, the journal of Formalized Mathematics (FM), and Mizar Mathematical Library(MML) are the exception, those Papers for which the final manuscripts were received by MMA-WiP.
In the case a decision is made not to publish in MMA-WiP as reject, MMA-WiP will return the copyrightfor such paper to the author.

7

1.4.3 Notes regarding copyrights transfer(a) In order to comply with copyright, you should obtain written consent from licenser to reprint withoutcharge if required.
(b) An article should include all coauthor’s name who contributor essentially.
(c) A consent or approval should be obtained prior to submission from an appropriate person who has
the authority of the author’s affiliate, if necessary.

1.5

Publishing translation papers

Authors are granted to publish their own English translation of an accepted paper in Mechanized
Mathematics and Its Applications (MMA).

2. Preparation manuscript

2.1 Important notices
The purpose of MMA-WiP is to become quickly and widely known as the results of new research,development, and applications that contribute to the science and technology of Mizar proof checking
system and MML libraries. Since valuable and exciting information for readers should be published in
the journal quickly and recognized efficiently, authors make manuscripts with following in mind.

(1) Notion or theories proposed in the article must be codified and verified by Mizar proof checking
system.
(2) Not only experts but also non-experts can understand the significance of contents and results.
(3) Manuscripts should be concisely presented without irrelevant content. The author must makesufficient elaboration to avoid typographical errors.
(4) Contents should be written logically without a gap in explanation. The validity of the prerequisite
assumption and condition for the paper should be considered enough. Moreover, its generality should
be shown.
(5) The current status of the related field would be summarized. The position of the paper there would
be appeared.
(6) The author would expressly represent which part is creativity or originality or significance in thepaper.

8

2.2 Language
Only Japanese or English language is considered for publication. Mizar article must be codified into
Mizar language and verified by Mizar proof checking system. For Article Paper, the language of thetext must be English.

2.3 Manuscript style and number of pages
Manuscript style and the number of pages for paper and letter are shown in following Table.3 and 4,
respectively.

Table 3. Manuscript style and number of pages for Regular Paper and System Development paper
Title

The paper title must be able to image the work.
The contents of the paper are accurately summarized. About 100 words.
For Article Paper, the language of the text should be English. A one-page

Abstract

abstract describing the contents of the paper should be included as acover page (required). A Japanese abstract may also be included.
It should be concisely written and can be easily understood, such as theconcept, purpose, reason, method, conclusion.

Manuscript
Style

Introduction

Necessity/significance of the research, the current status / the position of
the research in related fields, the purpose and the scope of the research,and the point of the originality should be represented without a body ofthe paper.

Conclusion
LengthAchievements against purpose, assertions of study, and future works
should be summarized.

of The number of pages must be 8(min)-16(max). However, the maximum

manuscript

number of pages for an article is not set for Article Paper.

Table 4. Manuscript style and number of pages for Letter
Title
Abstract
Manuscript Introduction
Style

It encourages that the content of the Letter is generally understood.

Conclusion
Lengthofmanuscript

The number of pages must be 4(min)-8(max)92.4 Manuscript Format
Manuscript format for Paper and Letter submitted to the MMA-WiP (hereinafter referred to as“Papers”) is exhibited in this chapter.

2.4.1 Manuscript preparation
All manuscript should be prepared using the LaTeX style file or MS-Word Template for the MMAWiP provided by the MMA-WiP as a general rule. The MMA-WiP LaTeX Style File and MS-Word
Template are available from the following MMA-WiP site; http://mizar-jp.org/journal/MMA-WiP
Please follow the instructions below when preparing the manuscript using the MMA-WiP LaTeX
Style File or MS-Word Template.
(1) Figures and photographs should be electronically included in the manuscript.
(2) The MMA-WiP LaTeX Style file and MS-Word Template distributed should not be modified.

2.4.2 Manuscript Structure
The manuscript should consist of the following contents (1)-(16) in the order as specified below.
Please format a manuscript in reference to a sample image PDF file of the published paper included in
the template file.
(1) Type of manuscript: Regular Paper, System Development Paper, Article Paper, or Letter(2) Japanese title (for Japanese paper only)(3) English title(4) Name(s) of the author(s) in Japanese (for Japanese paper only)(5) Name(s) of author(s) in English(6) Affiliation(s) and address(es) in Japanese (for Japanese paper only)(7) Affiliation(s) and address(es) in English(8) The mailing address of the corresponding author(9) Mizar Version, MML Version (not necessary for a letter)(10) Abstract (in English. about 100-200 words for a paper, within 100 words for a letter)(11) Already appearance or in submission elsewhere (if any)(12) Body of the manuscript (citation at least one Mizar article or MML, for a paper)(13) Acknowledgments (if any)(14) References(15) Mizar article information（for a paper）(16) The abstract file of Mizar article in (15) written by listing style. For Article Paper, only the contents
of files that have passed the Mizar proof checker (****.miz, ***.voc) will be published.

10

2.4.3 Body of the manuscript
The body of the manuscript should be written in the following order.
Section:1 *********
Subsection:1.1 *********

2.4.4 References(1) References are not only the author’s own related papers but also written by other papers. Any
supplementary materials of the papers cannot be attached at submission.
(2) All references should be numbered and listed at the end of the main text, and the numbers should be
noted in the main text with a parenthesized number in superscript, where the reference is made in
the main text.
(3) Committee report or company report which are not published in the general public should not be
included in the references.
(4) Papers in submission elsewhere are not appropriate.
(5) In principle, references are written in English. In the case that Japanese reference is cited in Japanese
paper, Japanese and English titles should be written. The names of all authors must be listed. Do not
omit the title of the paper. Japanese author names should be full names. For more detail, please see
the distributed template file.

2.4.5 Program list, Mizar article, Figures, Photographs, and Tables(1) The program list and Mizar article should be full page width beyond the body width and written
inline in the text.
(2) The title of the program list and Mizar article (MML identifier, serial numbers of theorem ordefinition) should be written in English and left-justified at the top of the list.
(3) Figures, photographs, and tables should be fitted as figure and table style respectively, and bodywidth, and written inline in the text.
(4) The title of figures, photographs, and tables should be left-justified at the bottom.
(5) All legend in the figure, photographs, and tables must be in English.
(6) The number of program list, Mizar article figures, photographs, and tables must be a serial number.

2.4.6 Attachment of verified Mizar article and support files
Notion or theories proposed in the article must be codified and verified by the Mizar proof checking
system. The author should create the abstract file and pre-load file, store them into a designated folder,and finally submit it with the manuscript.

11

See the template file representing the folder arrangement of support files and attachment method by
ZIP compression archive.

3. Process for Initial Submission of a Manuscript and Review Process

3.1 Process for Initial Submission of a Manuscript
Authors and Mizar-JAPAN contact concerning submission, receipt, review, resubmission, evaluation,and submission of the final manuscript of papers by the only email. Email address is listed on thefollowing MMA-WiP site; http://mizar-jp.org/journal/MMA-WiP

3.2 Submission
Information specified in the template must be provided. Then, the manuscript (and support files as
Mizar article) should be compressed and sent ZIP archive file. If the paper or the article has beenpreviously published in printed publications other than the released publications and is non-problematicwith respect to copyright laws, the published manuscript must be attached to the manuscript submitted
to the MMA-WiP.

3.3 Receipt, Review, Resubmission, and Evaluation
The committee of MMA-WiP will email receipt confirmations and inquiries about the submitted
paper.
(1) The paper and article submitted are confirmed the registration information by the committee of
MMA-WiP, and the author will receive an acknowledgment receipt with a paper ID. However, whena paper or an article deviates significantly from the instructions described in these guidelines, thepaper or the article will not be accepted. Furthermore, any replacement of the papers and articles
would be rejected once they submitted. Any change and addition of the authors would also be rejectedonce they submitted.
(2) The paper and article submitted will be reviewed in accordance with the “Rules for review criteria”
by one or two or more reviewers. Based on the comments of the reviewers, the editor in chief
evaluates the paper and article and reports the results to the chairperson of the Editorial Affairs
Committee. The chairperson of the Editorial Affairs Committee, in the committee of MMA-WiP,
based on this evaluation report, decides acceptance or rejection as categorized below, and then notify
the author accordingly.
Evaluation A: Accept
Evaluation B: Publish with minor revision. (Accept after minor revision)

12

Evaluation C: Refer back to the authors for clarifications before the decision on acceptance.
(Review after major revision)
Evaluation D: Not to be published. (Reject)(3) The author who received Evaluation B or C from reviewers should revise a manuscript and must
submit a revised manuscript with a response to the reviews and requirements within two months
after receipt of the evaluation report. All corrected places in revised manuscripts should behighlighted or written in red for easy identification. In addition, the author should clarify the contents
and locations of corrections per each inquiry from reviewers. Papers may be regarded as withdrawn
by authors when authors do not submit a revised manuscript within two months after receipt of theevaluation report. Submission of the revised manuscript after the completion of withdrawal
procedures is considered as a new submission, and receipt, review, and evaluation will be treated in
the same way as the initial submission.
(4) Notification of acceptance will be sent to the author if the submitted manuscript is Evaluation A, andaccepted for publication in MMA-WiP.
(5) Notification of rejection will be sent with reasons for the rejection if the manuscript decided to be
Evaluation D. If unable to accept the reason for rejection, authors can file a written opposition up to
two times.
(6) Paper screening procedure follows the steps described above, and the committee of MMA-WiP shallnot be held responsible for any liabilities incurred.
(7) Paper and article submitted to the MMA-WiP must not be submitted to other journals.

3.4 Procedures Following Acceptance3.4.1 Submission of Final Manuscript
he author who receives the notification of acceptance must register the necessary information (onlywhen instructed by the committee of MMA-WiP) and submit the final manuscript. The following final
manuscript data should be stored in a compressed folder and sent to the MMA-WiP.
(1) A set of manuscript data files (LaTeX, MS-Word and all other files)(2) Support files (e.g., Mizar article)(3) Typeset example for the paper (PDF file)

3.4.2 Proof-reading by the author
As a general rule, the author will be asked to proof-read the final copy only once.

13

4．Article-Processing Charge and Publication Fee
It is free of Article-Processing Charge and Publication Fee.

14

Revision record:
September 18, 2019

Drafting

September 24, 2019

Editorial Committee approval 1st edition

April 7, 2020

Drafting 1st edition in English

April 14, 2020

Editorial Committee approval 1st edition in English

September 23, 2021

Editorial Committee approval 2nd edition in English(Below margin)

15