MMA-WiP 論⽂誌

投稿の⼿引き［第 1 版 2019 年（令和元年）9 ⽉ 論⽂編集委員会 2019.9.24 承認］［第 2 版 2021 年（令和 3 年）9 ⽉ 論⽂編集委員会 2021.9.23 承認］

名称：Mechanized Mathematics and Its Applications, Works in Progress
略称：MMA-WiP

⽬ 次
1. 投稿規則2. 原稿の作成
3. 投稿⼿続きと原稿の取り扱い
4. 掲載料

１．投稿規則1.1 論⽂誌の発刊コンセプト

論⽂誌の発刊コンセプト（と掲載要件）:
本誌 MMA-WiP 発刊のコンセプトは現在進⾏中の研究（Works in Progress）を研究者間でタイムリーに共有する場を設けることにある. MMA-WiP での論⽂掲載についての基本的な考え⽅は，従前のMechanized Mathematics and Its Applications（以下 MMA）論⽂誌と同じく検証済 Mizar アーティク
ルを基礎としていることにある．しかしながら，速報性を重視し以下を掲載要件（の⽬安）として採⽤することとする．
以下，⼀般論⽂，システム開発論⽂，アーティクル論⽂，レターの総称も論⽂という．

論⽂：(1) 提案される概念の，Mizar プルーフチェッカによる検証通過は必須とする(2) 過去の検証済 Mizar アーティクルまたはプルーフチェッカのシステムを利活⽤した応⽤アプリケーションや援⽤ツールの内容も可とする（システム開発論⽂）(3) 速報性を重視したレビューを⾏い，オンライン出版(PDF)とする(4) プルーフチェッカで検証通過した概念は，mizar-jp.org が管理する [公開リポジトリ] に アーティクルファイル群を収納し，再利⽤性を⾼める（アーティクル論⽂）(5) 投稿・レビュー中・オンライン後に関わらず，年 1 回の Mizar 研究会（毎年末で開催予定）で講演を⾏っていただく1

(6) プルーフチェッカで検証通過した概念は，ポーランド Mizar チーム発⾏ Formalized Mathematics
への投稿・採録を⽬指す(7) Mizar Mathematical Library (MML) 収録後，新たな Mizar プルーフチェッカならびに MML バージョンがリリースされた後，mizar-jp.orgが管理する公開リポジトリから当該アーティクル群はMML 本体へマイグレーション(吸収)される

レター：論⽂と同⼀の範囲・内容を対象として，(8) プルーフチェッカで検証通過した概念の研究速報(9) 論⽂誌記事に対し意⾒を述べる紙上討論(10) 研究に関連して抱いた問題意識を述べる問題提起のいずれかの形式により新しい話題を提供し合う場である．

1.2 投稿の種別と要件

本論⽂誌は「⼀般論⽂」「システム開発論⽂」「アーティクル論⽂」「レター」の投稿を受け付ける．
これらは各々以下 1.2.1 から 1.2.4 の内容について，表 1, 2 に記載する各要件を満たし，内容が研究者倫理・技術者倫理に抵触しないものでなければならない．

1.2.1 新規性について・提案される概念が，既に証明済の MML ライブラリから trivial に導けないこと．
・システム開発論⽂については，既存技術の統合であっても，(a)組合せの新しさ，(b)システムの新しさ，(c)開発したシステムで得られた知⾒の新しさ，などを対象とする．
・著作権を遵守する．⼆重投稿等はこれを禁ずる．

1.2.2 有効性について・提案される概念が，Mizar の発展において何らかの意味で貢献できる内容であること．
・その論⽂で扱っている概念の重要性と，その論⽂で得られた成果（証明済 Mizar アーティクル）が，MML ライブラリにどの程度貢献しているか，あるいは今後貢献するかの度合を対象とする．
・システム開発関連の研究では，類似のシステムの評価データが公開されていない，あるいは公開されていても開発したシステムと同じ条件で評価することが難しい場合が少なくない．このような場合は，類似システムと⽐べて総合的あるいは部分的に優れていることが了解できる程度に記述されていることが必要となる．

1.2.3 信頼性について・提案される概念が，Mizar プルーフチェッカによる検証通過済であること．

2

・システム開発関連の研究では，計算や実験の過程を逐⼀たどるようなことは要求されない．論⽂を信頼性のあるものに仕上げるのは著者の責任であり，それが真⾯⽬に実⾏されていれば⾃然に信頼感を与えるものである．次の諸点にも留意して，なるべく客観的に判断できるようにすること．
・重要な⽂献が落ちなく引⽤され，公平に評価されているか．
・従来の技術や結果との⽐較・評価が⼗分になされ，適正な結論が導かれているか．
・理論・計算機実験・バックテスト等による裏付けに⼗分の努⼒が払われているか（ただし，分野によってはアイデアが⼗分に優れていれば，裏付けの⼗分性はそれほど問わない）
・実験の条件が明確に記述されているか，等．

1.2.4 了解性について・論旨の展開が⼗分理解できるように，分かりやすく，順序⽴てて，明瞭に記述してあること．
・システム開発論⽂については，技術的意味や解釈が述べられ，読者が納得できる形にまとめられていること．
・アーティクル論⽂については，Mizar プルーフチェッカを通過したファイル群（****.miz, ***.voc）の内容をそのまま掲載する．そのため，環境部や本体部の記述については，Mizar 援⽤システムが提供する各種ユーティリティを使⽤して，不要な引⽤や証明ステップを可能な限り削除しておくこと（http://mizar.org/library/submit.html に記載されている⼿順を参考とせよ）．

表 1. 論⽂の内容と要件
項⽬

内容

要件（論⽂）
掲載論⽂の基本的な考え⽅は，従前のMechanized Mathematics and Its Applications（MMA）論⽂誌と同じとする．
提案される概念の，Mizar プルーフチェッカに内容が Mizar に関係するものである
分野よる検証通過は必須とする．

こと．

過去の検証済 Mizar アーティクルまたはプルーフチェッカのシステムを利活⽤した応⽤アプリケーションや援⽤ツールの内容も可とす
る（システム開発論⽂）

新規性

主要な内容が，公知・既発表でない論⽂の内容が，既に証明済の MML ライブラリこと．また，既知のことから容易にから trivial に導けないこと．

は導き得ない新しいものであるこシステム開発論⽂については，既存技術の統合と．

であっても，(a)組合せの新しさ，(b)システム3の新しさ，(c)開発したシステムで得られた知⾒の新しさ，などが対象となる．
論⽂で扱っている概念の重要性と，その論⽂で得られた成果（証明済 Mizar アーティクル）が，MML ライブラリにどの程度貢献しているか，概念や内容が，Mizar の発展におい有効性あるいは今後貢献するかの度合を総合的に評て何らかの意味で貢献できる内容で価する．

あること．

システム開発論⽂では，類似システムと⽐べて総合的あるいは部分的に優れていることが了解できる程度に記述されていること．
システム開発論⽂では，どのような環境・条件提案される概念が，Mizar プルーフのもとに，どのような技術を統合したものであチェッカにより検証通過しているこ
信頼性り，それによってどのような結果が得られたかと．

が明確に記述されていれば，信頼性があると考えることができる．
システム開発論⽂については，技術的意味や解釈が述べられ，読者が納得できる形にまとめられていること．
論旨の展開が⼗分理解できるよう

アーティクル論⽂については，Mizar プルーフ
チ ェ ッ カ を 通 過 し た フ ァ イ ル 群 （ ****.miz,

了解性に，分かりやすく，順序⽴てて，明***.voc）の内容をそのまま掲載する．環境部や瞭に記述してあること．
本体部の記述については，Mizar 援⽤システムが提供する各種ユーティリティを使⽤して，不要な引⽤や証明ステップを可能な限り削除すること．

表 2. レターの内容と要件（分野と内容は表 1 と同⼀）要件（レター）

判定項⽬

研究速報

紙上討論，問題提起（アーティクルの速報性を重んじる）（討論により読者の問題意識を⾼めることをねらいとしている）

新規性

最も必要とされる

さほど⾼くなくてもよい

有効性

必要

上記の ねらい に合っていること

4内容が Mizar プルーフチェッカ，MML ラ
信頼性

Mizar プルーフチェッカにより検証通

イブラリあるいは援⽤システムの技術的範過していること

囲内であって，個⼈的感情にとらわれていないこと

論旨の展開が⼗分理解できるように，分かりやすく，順序⽴てて，明瞭に記述してあ了解性ること．論⽂ほどまとまっている必要はない．

1.3 公開出版物の定義

本⼿引における「公開出版物」とは，国内外で市販されている書籍・雑誌，ならびに査読を経て論⽂が掲載される学協会の刊⾏物を指す．なお，「公開出版物」以外の刊⾏物において発表された著作権法上，問題のない論⽂等を，新規の論⽂・レターとして投稿することは差し⽀えないが，既発表であることを投稿原稿中に明記するとともに，本会への投稿原稿に既発表の原稿を添付すること．ただし，本会が主催もしくは共催する研究会で発表された論⽂については，添付する必要はない．

1.4 著作権

1.4.1 著作権の帰属
論⽂誌に掲載される論⽂の著作権は本会に帰属する．よって，論⽂の投稿にあたって，著者は投稿時に⽇本国著作権法第 21 条から第 28 条までに規定されたすべての権利を本会に譲渡しなければならな
い．本会は著者が本会への電⼦投稿によって投稿したことをもって，著者全員が「MMA-WiP 論⽂誌への投稿⼿引」の著作権に関する記述を理解し，これに同意したものとみなす．電⼦投稿によって投稿できないものの著作権譲渡⽅法については，本会論⽂編集委員会に問合わせられたい．ただし，著作権を譲渡しても以下の権利等は著者の⼿元に残るものとする．
(a) 著作権以外の例えば特許権のような権利(b) 著者が⾃分の業績をまとめる際にその⼀部分として使⽤すること(c) 著者が営利を⽬的とせずに複写すること（例えば教育資料としての使⽤）(d) その他，⽇本国著作権法に反しない範囲で利⽤すること

1.4.2 他の公開出版物への投稿・発表同⼀内容の論⽂を，Formalized Mathematics 論⽂誌，Mizar Mathematical Library (MML) 以外の他の公開出版物に投稿・発表してはならない．ただし，論⽂が掲載不可となった場合，掲載不可の決定時点で本会への著作権の譲渡も無効となる．

1.4.3 著作権の譲渡にあたっての留意事項(a) 他の著作物からの引⽤にあたっては，著作権上の問題が⽣じないように⼗分に注意されたい．著作権許諾が必要な引⽤については，無償での転載許諾を書⾯で得なければならない．

5

(b) 内容に本質的な貢献を⾏った⼈はすべて著者に含めなければならない．
(c) 必要な場合には著者の所属機関のしかるべき権限を有する⼈の同意を得ていなければならない．

1.5 翻訳論⽂の出版

本会論⽂誌に掲載された⽇本語の論⽂を翻訳して Mechanized Mathematics and Its Applications（MMA）論⽂誌に掲載することを許諾している．

2．原稿の作成
2.1 留意事項

本会論⽂誌は，Mizar プルーフチェッカならびに MML ライブラリに関する学術・技術に寄与する
新しい研究・開発ならびに応⽤の結果を速やかに広く伝えるための場である．投稿者は読者にとって価値があり，興味ある情報を効率よく伝えるため，また速やかに誌上に掲載するために，次の点に留意して原稿を作成されたい．

(1) 提案される概念の，Mizar プルーフチェッカによる検証通過は必須とする．
(2) 同じ専⾨分野の読者はもちろん，専⾨外の⼈にも発表内容の意義と成果が理解できるようにする．
(3) 本質に関係のないことは省き，簡明に表現する．誤字や脱字がないように推敲を重ねる．
(4) 論⽂の内容は論理的に配列し，説明に⾶躍があってはならない．特に論⽂の前提となる仮定や条件の妥当性について⼗分検討し，⼀般性のあることを明らかにする．
(5) 関連した分野の現状をまとめ，発表内容の位置づけを明らかにする．
(6) 論⽂の発表内容のうち，どの部分に創造性，新規性，有⽤性などがあるかを明確に表現する

2.2 ⾔語

⽇本語または英語に限る．Mizar アーティクルは Mizar ⾔語により，プルーフチェッカによる検証通過は必須とする．アーティクル論⽂については，本⽂の⾔語は英語を原則とする．

2.3 論⽂・レターの体裁とページ数の制限

論⽂・レターの体裁とページ数の制限は表 3,4 の通りとする．

表 3. 論⽂の体裁とページ数制限
題名
体裁論⽂の内容が容易に想像しうるものであること

英⽂アブス
本論⽂の内容を正確に要約していること．100 ワード程度．
トラクト

6アーティクル論⽂については，本⽂の⾔語は英語を原則とする．カバーページとして，論⽂内容を表した one page abstract を記載すること（必須条件）．なお，⽇本語アブストラクトを付けてもよい．
概念・⽬的・理由・⼿法・結論など容易に理解できるように簡明に書かれていること．
研究の必要性・意義・関連分野における従来の研究状況とその中での本研究の位置づ
まえがき

け，⽬的と取り扱う範囲，オリジナリティを主張する範囲が本論に⽬を通さなくても理解できること．
⽬的に対する到達レベル，研究の主張点のまとめ，今後の課題・計画について要約しむすびてあること．

仕上がりペ

最⼩ 8 ページ，最⼤ 16 ページ以内を標準とする．ただし，アーティクル論⽂についてージ数は，論⽂の仕上がりページ数の最⼤は，これを設定しない．

表 4. レターの体裁とページ数制限
題名
英⽂アブス
トラクト
体裁

⼀般に理解できるように記述されていればよい

まえがきむすび仕上がりペ
最⼩ 4 ページ，最⼤ 8 ページ以内を標準とする
ージ数

2.4 原稿の様式

本会論⽂誌に投稿する論⽂・レター（以後，「論⽂等」と称する）の原稿の様式を本章で定める．

2.4.1 原稿の作成⽅法
原則として，本会が⽤意する本会論⽂誌のための LaTeX ⽤スタイルファイルもしくは MS-Word ⽤テンプレートを利⽤して原稿を作成すること．これらは次の Web ページからダウンロードすることができる；MMA-WiP 論⽂誌ポータル http://mizar-jp.org/journal/MMA-WiP
なお，上記の LaTeX ⽤スタイルファイルと MS-Word ⽤テンプレートを利⽤する際は，次の点に注意されたい．

(1) 図⾯，写真は電⼦的な形で原稿中に取り込むこと(2) 配布されたスタイルファイルおよびテンプレートを修正しないこと

7

2.4.2 原稿の構成
論⽂等の原稿は次の(1)〜(16)の内容，順序で構成する．なお，刷り上がり紙⾯のサンプルイメージ
PDF ファイルがテンプレート配布ファイルに同梱されているので，参考にして体裁を整えること．

(1) 論⽂分類：⼀般論⽂（Regular Paper），システム開発論⽂（System Development Paper），アーティクル論⽂（Article），レター（Letter）の別(2) ⽇本語の表題（⽇本語の論⽂等のみ）(3) 英語の表題(4) ⽇本語の著者⽒名（⽇本語の論⽂等のみ）(5) 英語の著者⽒名(6) ⽇本語の著者所属機関名，所属機関のアドレス（⽇本語の論⽂等のみ）(7) 英語の著者所属機関名，所属機関のアドレス(8) 連絡著者の電⼦メールアドレス(9) Mizar プルーフチェッカのバージョンと MML のバージョン番号（論⽂の場合）(10) Abstract（英語で書く．論⽂の場合 100〜200 語以内，レターの場合 100 語以内）
(11) 既発表であることの明記（必要な場合のみ）(12) 本⽂（論⽂の場合は，最低 1 報以上の Mizar アーティクル, MML の引⽤が必要）(13) 謝辞（必要な場合のみ）(14) 参考⽂献(15) Mizar article information（Works in Progress，論⽂の場合）(16) (15)で⽰した Mizar アーティクルの abstract ファイルを listing で引⽤したもの．アーティクル論⽂については，Mizar プルーフチェッカを通過したファイル群（****.miz, ***.voc）の内容をそのまま掲載する．

2.4.3 本⽂の記述
本⽂の記述は下記の順序に整理する．
章：1 ○○○○○○
節：1.1 ○○○○○○

2.4.4 ⽂献
(1) 著者⾃⾝の関連論⽂のみならず，著者以外の論⽂等著作物等を含め，適切かつ⼗分な参考⽂献をあげること．なお，論⽂等の内容を補⾜する資料を投稿時に添付することはできない．
(2) ⽂献は，論⽂等の本⽂末尾に通し番号をつけて⼀括記載し，本⽂中の該当箇所に⾓カッコで囲んだ引⽤番号を記⼊すること．
(3) ⼀般に公表されていない委員会報告や社内報告などは⽂献としてあげないこと．

8

(4) 投稿中の論⽂等は引⽤しないこと．
(5) ⽂献は原則として英語で記載すること．ただし，⽇本語の論⽂等において⽇本語の⽂献をあげる場
合は原則として⽇本語と英語の表記を併記すること．著者名は著者全員を記載し，論⽂等のタイトルを省略してはならない．なお，⽇本語の表記では，著者名をフルネームで記載すること．具体的なフォーマットはテンプレート配布ファイルを参照されたい．

2.4.5 プログラムリスト，Mizar アーティクル，図⾯・写真・表(1) プログラムリスト，Mizar アーティクルは，listing スタイルで本⽂幅を超えるページ幅いっぱいで，本⽂中インラインで記載する．
(2) プログラムリスト，Mizar アーティクルの表題（MML identifier, 定理・定義の通し番号）は，英語でリストの上部左詰めで記載すること．
(3) 図⾯・写真・表は，figure, table スタイル，本⽂幅，本⽂中インラインで掲載する．
(4) 図⾯・写真の表題は，英語で図⾯・写真の下部左詰めで記載すること．
(5) 図⾯・写真・表中の説明は，原則として英語にすること．
(6) プログラムリスト，Mizar アーティクル，図⾯・写真・表の番号は，それぞれ通し番号にすること．

2.4.6 検証済 Mizar アーティクル，サポートファイルの添付について論⽂の本⽂ファイルとともに，提案される概念は，実際に Mizar アーティクルを作成し，プルーフチェッカを通過させた後，abstract ファイルと pre-load ファイルの⽣成を⾏い，指定のフォルダへ配置した上，原稿ファイルに添付して提出すること．
各種サポートファイルのフォルダ配置と ZIP 圧縮書庫による具体的な添付⽅法は，テンプレート配布ファイルを参照されたい．

3．投稿⼿続きと原稿の取り扱い
3.1 投稿等の⼿続き論⽂等の投稿，受付，審査，再提出，判定，最終原稿の提出はすべて本会と電⼦メールによって⾏う．論⽂投稿の電⼦メールアドレスは，次の URL にアクセスして確認すること；
MMA-WiP 論⽂誌ポータル http://mizar-jp.org/journal/MMA-WiP

3.2 投稿

論⽂等を投稿する際は，テンプレート配布ファイルの指⽰に従って，投稿に必要な情報とともに，原稿（ならびに Mizar アーティクル等のサポートファイル⼀式）の ZIP 圧縮書庫ファイルを添付し送信する．公開出版物以外の刊⾏物において発表された，著作権法上，問題のない論⽂等を投稿する場合は，既発表の原稿をあわせて提出すること

9

3.3 受付・審査・再提出・判定

投稿論⽂に関する全ての受領確認と照会等は，論⽂編集委員会からメールで送信される．

(1) 投稿論⽂等は本会論⽂編集委員会が登録内容を確認した後，著者に受付番号等を通知する．本投稿⼿引の記載事項から逸脱した論⽂等は受け付けない．また，⼀度投稿された論⽂等の差し替えおよび投稿後の著者の変更・追加は⼀切認めない．

(2) 投稿論⽂等は 1 名ないし 2 名以上の論⽂査読者により「論⽂査読基準（申し合わせ）」に従って審査される．担当編集委員は，査読者からの審査意⾒に基づいて論⽂等に対する判定の取り纏めを⾏い，その結果を編集⻑に報告する．編集⻑は論⽂編集委員会を開催し，その判定結果に基づいて次のように採否などを決め投稿者に通知する．
判定 A 採録
判定 B 条件付採録（軽微な修正点はあるが投稿者に照会のうえ⼀部修正すれば掲載）
判定 C 照会（著者に照会して回答を求めたうえで採否を決める）
判定 D 返却（掲載不可）(3) 条件付採録・照会を受けた著者は，採録条件・照会に対する回答⽂を作成するとともに，内容に応じて投稿原稿を修正し，判定⽇後 2 ヶ⽉以内に修正済原稿，回答⽂を提出する．なお，修正済原稿には変更が判別しやすいように修正箇所を朱書きやハイライトなどし，回答⽂には，各事項に対してそれぞれ修正内容と修正箇所を明記すること．判定後 2 ヶ⽉を経過しても提出されない原稿は著者⾃⾝が投稿を取り下げたと⾒なす．取り下げ処理完了後に修正原稿を提出する場合は新規投稿扱
いとし，新規投稿同様の受付・審査・判定を⾏う．
(4) 掲載が決定した著者には掲載決定を通知する．
(5) 掲載不可が決定した著者には返却理由とともに返却決定を通知する．なお，返却理由に承服できない点がある場合は，同⼀論⽂について 2 回を限度に，書⾯による異議申し⽴てを⾏うことができる．
(6) 論⽂等の採否判定は上記⼿続きにより⾏われるものであり，本会論⽂編集委員会はこのことによって⽣じる不利益に対しての責任は⼀切負わない．
(7) 投稿中の論⽂等を他誌へ投稿してはならない。

3.4 掲載決定後の⼿続き

3.4.1 最終原稿の提出
掲載決定を通知された著者は，論⽂編集委員会からの指⽰がある場合には，掲載の際に必要な情報を登録するとともに，次の最終原稿データをひとつのフォルダに収めて圧縮し，提出する．
(1) 原稿データファイル⼀式（LaTeX, Word ファイル等）

10

(2) Mizar アーティクルなどのサポートファイル(3) 原稿完成⾒本（PDF ファイル）

3.4.2 著者校正
最終原稿については，原則 1 回の著者校正を⾏う．

4．掲載料

掲載料は，これを要しない．

11

改定記録：
2019.9.18

原案作成

2019.9.24

編集委員会承認 第 1 版

2021.9.23

編集委員会承認 第 2 版（種別「アーティクル」追加）（以下，余⽩）12