| 研究課題/領域番号 |
25610034
|
|---|
| 研究種目 |
挑戦的萌芽研究
|
| 研究機関 | 九州大学 |
|---|
研究代表者 |
溝口 佳寛 九州大学, マス・フォア・インダストリ研究所, 准教授 (80209783)
|
|---|
| 研究期間 (年度) |
2013-04-01 – 2015-03-31
|
| キーワード | 証明支援系 / 有限オートマトン / Coq / Isabelle / Mizar |
|---|
| 研究概要 |
本年度の具体的な研究成果のひとつは有限オートマトンとスティッカー系の形式化を行い従来手法でのミスを指摘し形式的に厳密な手法を提案したことである. 本成果はAFCA(1st Int. Workshop on Applications and Fundamentals of Cellular Automata)において公表し論文集に掲載されている. また, 2014年3月には日本数学会年会において講演発表も行った. その他, 変換理論に関する調査研究とサーベイを行い, 様々な関連分野の研究者との情報交換を行った. 特に, 組合せ数学, 離散数学に関する研究集会を3回, 論理と計算に関する研究集会を1回開催し関連分野の研究者らとの詳細な討論を行った. また, 具体的な定理証明系のシステムに関する情報交換をCoqについては産業技術総合研究所のAffeldt氏, 平井氏らと, Mizarについては信州大学の師玉教授, 中西氏と, そして, IsabelleについてはSheffield大学のStruth氏と今後の研究計画について打合せを行った.
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
グラフ変換の形式化に関するサーベイ, セルオートマトン関する単射性に関するサーベイ, 量子回路の簡約化に関するサーベイはほぼ終了し, 具体的な定式化として, 有限オートマトン, スティッカー系の形式化を行った. そして, 次の2件を公表した. (1) Formal Proofs for Automata and Sticker Systems, Proc. of First International Symposium on Computing and Networking, 563-566, 2013. (2) 有限オートマトンとスティカー系に関するCoqによる形式証明について, 日本数学会2014年度年かい応用数学分科会講演アブストラクト, 56-62, 2014. また, 来年度の課題についても今まで異なる分野や異なる研究会に所属していたが共通の目的意識を持つ研究者の方々と多くの研究者と知り合うことが出来, 充実した討論が行うことも出来た.
|
| 今後の研究の推進方策 |
自らの研究, オートマトンの形式化を推進するとともに, 数学の形式化に関する研究討論が出来る場を広げて行く予定である. 特に, 2014年12月には, 研究集会Theorem Proving and Prover's meetingを九州大学にて開催し, 自動検証可能なプログラム言語を開発中のCertifided Programming with Dependent Typesの著者であるMITのAdam Chipala氏を招聘しプログラム言語の立場から数学の形式化についての課題を一緒に考察する予定である.
|
| 次年度の研究費の使用計画 |
高速大量計算の必要性が生じたため, 当初予定よりも高性能の計算機を購入することにした. その納入時期が遅れたため, 次年度の購入となる.
2014年12月に3日間のTheorem Proving and Prover's meetingにおいて海外からの研究者を招聘するとともに, 国内外の研究者との積極的な討論を行う. その開催費用の一部を本科研費から支出する予定である.
|
