2013 Fiscal Year Annual Research Report
| Project/Area Number |
23700164
|
|---|
| Research Institution | University of Yamanashi |
|---|
Principal Investigator |
鍋島 英知 山梨大学, 医学工学総合研究部, 准教授 (10334848)
|
|---|
| Keywords | 結論発見 / 仮説発見 / 一階述語論理 / 命題論理 / 推論システム / 分割統治 |
|---|
| Research Abstract |
平成25年度は，24年度に新たに開発した最良優先探索に基づく結論発見システムに対して種々の改良を行った．具体的には，最良優先探索のためのタブローの深さ，幅，サブロールの一般性をもとにした新たな評価関数の実現，高速な項索引機構の実装を行った．また，最良優先探索では数多くのタブローを同時展開するため，それらの削減が非常に重要となる．そこで冗長なタブローを除去するために単位公理・単位補題マッチングの完全検査を実施し，大きな性能改善を得た．この知見から，補題の積極的な生成が重要になると考え，従来の閉じたサブタブローから補題を生成するだけでなく，タブローのオープンノードが１つであった場合に補題を生成する新たな手法を考案し，さらなる性能改善が得られることを実証した．また，冗長なタブローを抑制するため，持ち上げ補題と分岐補題を重複するサブタブローの削減だけでなく，矛盾を導出できないサブタブローの削減にも活用し，特に充足可能な問題の証明に対して効果があることを実証した．結論発見手続きSOLにおいて，タブロー数の増大をもたらす主要因は，タブローの拡張操作にある．これを改善するため，代入が等しい操作を１つにまとめ上げ，代入のみ適用して拡張操作を遅延評価する遅延拡張技術を考案した．どのような場合に遅延評価を行うか判断するヒューリスティクスが問題に依存する側面があるため，頑健な評価基準の構築はまだ実現できていないものの，一定の性能改善が得ることができた．この技術は組み込み述語などの導入においても基盤となるものである．これらの改善の結果，従来のトップダウン型結論発見システムを上回る性能向上を達成した．
また，命題版結論発見システムの基盤となる命題論理の充足可能性判定器について，バイナリ融合節に基づく軽量な動的簡単化手法を考案し，性能改善を達成した．
|
