2019 Fiscal Year Research-status Report
数理議論学に基づく仕様書の不整合解消支援ツールの作成
| Project/Area Number |
19K11914
|
|---|
| Research Institution | Sendai National College of Technology |
|---|
Principal Investigator |
岡本 圭史 仙台高等専門学校, 総合工学科, 教授 (00308214)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
高井 利憲 奈良先端科学技術大学院大学, 先端科学技術研究科, 客員准教授 (10425738)
木藤 浩之 電気通信大学, 大学院情報理工学研究科, 客員研究員 (90705287)
|
|---|
| Project Period (FY) |
2019-04-01 – 2022-03-31
|
| Keywords | 数理議論学 / 数理論理学 / SMTソルバ / 仕様 / 品質向上 |
|---|
| Outline of Annual Research Achievements |
平成31年度(令和元年度)の研究計画では，1)議論フレームワーク構築法の提案(令和二年度まで)，2)外延列挙法の提案(令和二年度まで)，および3)不整合解消支援手法の提案とツール試作・評価(令和三年度まで)の実施を計画していた．1と2は独立に進めることができるため，本年度は主に1と2について研究を実施した．
1)議論フレームワーク構築法の提案に関しては，数理議論学に基づく手法や自然言語処理に基づく手法を検討している．自然言語処理に基づく手法としては，文埋め込みを用いた手法を検討している．
2)外延列挙法の提案に関しては，外延の一階述語論理の拡張を用いた記述法を提案した．いくつかの外延は一階述語論理の枠組み内で記述できることが知られているが，集合の極小性・極大性が定義に要求されているため，いくつかの外延は一階述語論理の枠組み内では記述できない．他方，ツール試作に際し，述語論理ソルバ(SMTソルバ)を用いる予定である．そこで本研究では．一階述語論理の枠組み内で記述できない性質を
SMTソルバの拡張で実現できると思われるよう分離し，一階述語論理の拡張を用いて記述した．これにより，４つの拡張すべてが充足判定器SMTソルバを利用して抽出でき，
ソルバを拡張することで列挙も可能であると予想される．この成果は国内会議等にて発表し，論文が掲載予定である．
3)不整合解消支援手法の提案とツール試作・評価に関しては，SMTソルバによる抽出・列挙を試行中である．外延の抽出・列挙がツール上でも実現可能であることを示すことができれば，外延列挙法の提案として研究成果を公表し，ツールの試作を行う予定である．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
研究全体としての進捗状況は，令和元年度末に予定していた国際会議発表がキャンセルとなる等もあったが，おおむね予定通りの進捗状況であった．
1) 議論フレームワーク構築法の提案に関しては，本年度は数理議論学に基づく手法や自然言語処理に基づく手法を検討し，次年度も継続する．数理議論学や自然言語処理でいくつかの有用なアプローチがあるため，それらを実現・発展させることで，議論フレームワーク構築法の提案できると考える．
2) 外延列挙法の提案に関しては，本年度は外延の一階述語論理の拡張を用いた記述法を提案した．次年度に，本年度提案した外延の記述法を基に，SMTソルバを拡張することで，外延列挙法を提案できると考える．
3)不整合解消支援手法の提案とツール試作・評価に関しては，本年度はSMTソルバによる抽出・列挙を試行した．本年度の段階では簡潔な外延の抽出のみ実現したが，SMTソルバを拡張することで，全ての外延の列挙法に対するツールを試作できると考える．また，実際に仕様記述に携わるソフトウェア開発者らと連携することで，実用的な不整合解消支援手法を提案出来ると考える．
|
| Strategy for Future Research Activity |
令和二年度の研究計画では，1)議論フレームワーク構築法の提案(令和二年度まで)，
2)外延列挙法の提案(令和二年度まで)，および3)不整合解消支援手法の提案とツール試作・評価(令和三年度まで)を実施する．
1) 議論フレームワーク構築法の提案に関しては，次年度も数理議論学に基づく手法や自然言語処理に基づく手法を検討し，有用な手法の提案を行う．特に自然言語処理に基づく手法に関しては，最近の文埋め込みや文埋め込みを用いた応用研究が有用であると考えらえるため，これら用いた手法を検討・実験を主に行う予定である．
2) 外延列挙法の提案に関しては，本年度提案した一階述語論理の拡張を用いた記述法を基に列挙法を提案し，合わせてSMTソルバとその拡張により提案列挙法を実現する．極小・極大集合はSMTソルバによる抽出を繰り返し実行することで可能である．しかし，素朴な繰返しは計算量が膨大になるため，計算量を抑える工夫を調査・研究し，列挙法を提案する．
3) 不整合解消支援手法の提案とツール試作・評価に関しては，ソフトウェア開発者らと意見交換を行い不整合解消支援手法を検討し，合わせて1と2の進捗を元にツール試作・評価を行う．外延列挙ツールに関しては，次年度中の試作を目指す．
|
| Causes of Carryover |
コロナウィルスの世界的感染爆発により，発表が予定されていた国際会議が中止となったため，旅費等が発生しなくなり，次年度使用額が生じた．中止・延期となった国際会議参加のための旅費等，及びオンライでの会議参加のための諸費用に使用する予定である．
|
