前向き推論に基づく一階述語定理証明の効率化に関する研究

一階述語論理におてい前向き推論による定理証明の問題点をまとめた。前向き推論では発見した違反節を展開し,それぞれのサブケースに対して同様に処理する。そのため,証明に関連がない違反節を前向き推論に用いた場合,探索空間が爆発的に増大することがある。このような無駄な探索を防止するために,証明に関連がある節だけを推論に用いる方法が提案されている。しかし,これまで提案した関連節の判断基準は非ホーン節の頭部に現れるすべてのアトムは導出可能とされている。しかし,節の本体のアトムは導出できなければ頭部アトムも導出できないので,これまでの関連節の判断基準は不完全であることが判明した。我々は節集合に含まれているすべてのアトムに対してその節集合において導出可能かどうかを計算するアルゴリズムを提案した。あるアトムは節集合から導出可能かどうかを判断するとき,後向き推論を用いて行う。そして,導出可能なアトムだけを関連アトムに関する判断に用いる。多くの場合において,関連アトムの数が減少するので,前向き推論に用いる関連節の数も減少する。そのため,探索空間を一層制限することが実現した。また,我々はProlog言語を用いて提案したアルゴリズムをワークステーションの上に実装した。そして,自動定理証明システムの性能を検証するベンチマーク問題を用いて提案した手法の効率性について実験を行った。その結果,提案した手法は無駄な探索空間をカットできたことが分かった。本研究の研究結果はJournal of Computer Science and Technologyにて発表した。

一階述語論理におてい前向き推論による定理証明の問題点をまとめた。前向き推論では発見した違反節を展開し,それぞれのサブケースに対して同様に処理する。そのため,証明に関連がない違反節を前向き推論に用いた場合,探索空間が爆発的に増大することがある。このような無駄な探索を防止するために,証明に関連がある節だけを推論に用いる方法が提案されている。しかし,これまで提案した関連節の判断基準は非ホーン節の頭部に現れるすべてのアトムは導出可能とされている。しかし,節の本体のアトムは導出できなければ頭部アトムも導出できないので,これまでの関連節の判断基準は不完全であることが判明した。我々は節集合に含まれているすべてのアトムに対してその節集合において導出可能かどうかを計算するアルゴリズムを提案した。あるアトムは節集合から導出可能かどうかを判断するとき,後向き推論を用いて行う。そして,導出可能なアトムだけを関連アトムに関する判断に用いる。多くの場合において,関連アトムの数が減少するので,前向き推論に用いる関連節の数も減少する。そのため,探索空間を一層制限することが実現した。また,我々はProlog言語を用いて提案したアルゴリズムをワークステーションの上に実装した。そして,自動定理証明システムの性能を検証するベンチマーク問題を用いて提案した手法の効率性について実験を行った。その結果,提案した手法は無駄な探索空間をカットできたことが分かった。本研究の研究結果はJournal of Computer Science and Technologyにて発表した。