| 研究課題/領域番号 |
18K11154
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分60010:情報学基礎論関連
|
|---|
| 研究機関 | 千葉大学 |
|---|
研究代表者 |
山本 光晴 千葉大学, 大学院理学研究院, 教授 (00291295)
|
|---|
| 研究期間 (年度) |
2018-04-01 – 2024-03-31
|
| 研究課題ステータス |
完了 (2023年度)
|
| 配分額 *注記 |
2,470千円 (直接経費: 1,900千円、間接経費: 570千円)
2022年度: 390千円 (直接経費: 300千円、間接経費: 90千円)
2021年度: 390千円 (直接経費: 300千円、間接経費: 90千円)
2020年度: 650千円 (直接経費: 500千円、間接経費: 150千円)
2019年度: 390千円 (直接経費: 300千円、間接経費: 90千円)
2018年度: 650千円 (直接経費: 500千円、間接経費: 150千円)
|
|---|
| キーワード | 定理証明支援系 / 形式化 / ベクトル加算系 / 到達可能性 / ペトリネット |
|---|
| 研究成果の概要 |
ベクトル加算系およびそれと等価な状態遷移系における到達可能性問題周辺のいくつかの問題について形式化を完成させた。具体的には、ペトリネットの有界性問題および停止性問題に関する形式化、状態付きベクトル加算系からベクトル加算系への到達可能性を保存する変換の形式化である。ベクトル加算系における到達可能性問題の決定可能性については形式化の完成を見なかったが、この問題に対する様々な証明手法を調査し、形式化に有望な手法に関する知見を得た。
|
| 研究成果の学術的意義や社会的意義 |
定理証明支援系を用いた形式化によって、機械的に検査された正しい証明が得られるだけでなく、一旦完了した証明に対する試行錯誤や適切な抽象化の検討がしやすくなる。本研究の成果の一部である状態付きベクトル加算系からベクトル加算系への変換の形式化においても、適切な抽象化を行うことで元の証明に用いられていた変換が改良された。
また、形式化の過程で構築・蓄積された技術やノウハウは、後に別の定理を形式的に証明する際の道具として生かされる。上記の変換の形式化においてもベクトルの回転に関するライブラリが整備された。
|
