研究の成果

(1) 研究上の成果

○ ケース分割の重複削除手法

MGTPのモデル生成過程においてケース分割によって証明木の枝が分岐すると、 分岐後の各枝で同じ証明を重複して行なってしまい、その結果、探索空間が増 大し、証明時間も長くなってしまう恐れがある。このようなケース分割の重複 証明を除去する手法としてLetzがタブロー法の枠組でFactorizationと Folding-upを提案している。

Factorizationは、「ある部分証明を他の部分証明に委ねる」という考えに基 づいており、Folding-upは、「部分証明から補題を抽出し、それを他の部分証 明で利用する」という考えに基づいている。前者の枝刈りを後者は模擬できる がその逆はできない、という点で、後者の方が強力な枝刈り手法である。

前年度は、Factorizationを節変換によって実現するFolding-downを実装し良 好な結果を得た。今年度はMGTPの枠組でFolding-upを実現する方法を検討した。 それには、推論の依存関係を計算する機構をMGTPに組み込む必要があり、その 安価で効率的な実装法を考案した。さらにこの計算機構を利用すると、NHM (前年度の成果)で実現された関連性テストの機能(証明に無関係な分岐を抑制 する)と類似の枝刈りが、容易に実現できることが判明した。

TPTPライブラリ(定理証明システムのための問題集)からノンホーン(証明に分 岐を含む)問題77題を用いて本方式の評価実験を行ったところ、26題で顕著な 証明時間削減効果が確認された。

○ NHMの効率化手法

NHMは、証明に寄与しない推論を抑制するように、節変換を証明に先だって行 う手法である。前年度に作成した深さ優先変換をTPTPライブラリの問題に適用 したところ、顕著な枝刈り効果を示す問題がある一方、期待に反し、証明時間 が増大する問題が見られた。その原因には、探索の非決定性からくるものの他 に、(1)変換後の節数が一般的に増加することと、(2)関連性テストを行うた めの制御述語による証明図の巨大化、があることが判明した。

(1)は、値域限定性を保持する目的で導入された修飾子の数の多さに起因して いる。そこで、極小な修飾子のみを変換に用いるようにする極小束縛NHM変換 を考案した。深さ優先と幅優先変換に本手法を取り入れ実験を行ったところ、 NHM効果を保持しつつ、節数が削減できることを確認した。 (2)の要因に対しては、次に述べる高速データ検索によって対処した。

○ 高速データ検索による推論速度の高速化

MGTPの基本演算である連言照合と包摂検査では、内部データベースに対する二 つの検索操作、matchable(照合するデータを検索)とidentical(一致するデー タを検索)の二つの操作を煩雑に利用する。これらの操作の効率的実装は、推 論速度の向上に欠かせない。そこで、これらの操作を高速に行うことで定評の ある弁別木プログラムを実装し、MGTPに組み込んだ。

一般の弁別木プログラムは、格納するデータに変数が含まれているものとして 処理を行っているが、MGTPで格納するデータには変数は含まれないので、変数 に関わる処理を省略することができ、より効率的なプログラムを作成すること ができた。TPTPライブラリの問題の内、証明に10秒以上要する74題を用いて、 弁別木プログラムによる証明時間短縮効果を調べたところ、証明木が低い1題 を除いて効果が確認できた。

○ 項書換え処理のMGTPへの組み込み

等号推論をMGTPに組み込む第一段として、項書換え処理をMGTPに組み込んだ。 今のところ項書換え規則は、ユーザが予め与えたものに限っている。一般の等 号推論(paramodulation)に比べ、項書換え処理は、書換え途中のアトムを保持 しないので、内部データベースのサイズを小さく抑えられるという利点がある。

項書換え規則をMGTP節と併用する事により、より自然な問題記述が可能となっ た。加えて、ある種の例外処理も容易に記述することができるようになった。

○ GAを組み込んだMGTPによるCondensed Detachment問題の解法

GA(遺伝的アルゴリズム)とモデル生成法は、手続き的に非常に類似している。 初期世代が正節に、最終世代が生成したモデルに、中間世代がモデル候補に、 そして、交叉が連言照合とモデル拡張に対応しているものと見なせる。この類 似性に着目し、Condensed Detachment問題をGAを組み込んだMGTPによって解く 手法を検討した。Condensed Detachment問題を選んだのは、モデル拡張規則が 一つしかなく取り組みやすいと考えたからである。実験の結果、GAが有効とな る問題もあることを確認した。

○ 外部発表論文リスト

【1】長谷川 隆三，越村 三幸，井上 克巳，太田 好彦 :

上昇型定 理証明のためのノンホーン・マジックセット、 九州大学大学院システム情報科学研究科報告，第1巻，第1号， pp.85-90 (1996)

【2】田中 智浩，越村 三幸，長谷川 隆三 :

ノンホーン・マジックセット変換の妥当性と効率化， 第4回電子情報通信学会九州支部学生会講演会，pp.80 (1996)

【3】松本 誉史，越村 三幸，長谷川 隆三 :

MGTPにおけるケース分割の重複削除手法とその評価， 第4回電子情報通信学会九州支部学生会講演会，pp.81 (1996)

【4】Ryuzo Hasegawa:

``A Method to Enhance the Search Efficiency by Combining Relevancy Testing and Folding-up Strategies'', Dagstuhl-Seminar on Deduction (1997)

【5】長谷川 隆三，井上 克巳，太田 好彦，越村 三幸 :

上昇型定理証明の探索効率を高めるノンホーン・マジックセット， 情報処理学会論文誌，第38巻，第3号，(1997) (掲載予定)

【6】松本 誉史，越村 三幸，久保山 哲二，長谷川 隆三 :

MGTPにおけるケース分割の重複削除手法とその評価， 九州大学大学院システム情報科学研究科報告，第2巻，第1号 (1997) (掲載予定)

【7】久保山 哲二，松本 誉史，長谷川 隆三，雨宮 真人 :

動的補題生成法を用いたモデル生成木の枝刈り手法とその実装， 九州大学大学院システム情報科学研究科報告，第2巻，第1号 (1997) (掲載予定)

【8】Ryuzo Hasegawa, Hiroshi Fujita and Miyuki Koshimura:

``MGTP: A Model Generation Theorem Prover -Its Advanced Features and Applications-'', to appear in Proc. of TABLEAUX'97 (1997)

【9】Ryuzo Hasegawa, Katsumi Inoue, Yoshihiko Ohta and Miyuki Koshimura:

``Non-Horn Magic Sets to Incorporate Top-down Inference into Bottom-up Theorem Proving'', to appear in Proc. of 14th Int. Conf. on Automated Deduction (1997)

(2) ソフトウェアとしての成果

○ 新規作成ソフト

1. Folding-up機能付きMGTP： コンパイラ版とインタプリタ版の 双方を作成。
2. 項書換え機能付きMGTP： 項書換え規則を扱えるようにMGTPを 変更し、また例外処理機能も加えた。
3. インタプリタ版CMGTP： 機能拡張したインタプリタ版MGTP(下記 参照)をベースに作成。
4. MGTPWM： マウス操作によってMGTPのオプション指定や起動が できるウィンドウマネージャ(図1参照)をTcl/Tkで作成した。

図 1: MGTPウィンドウマネージャ

○ 既システムの整備

前年度の成果ソフトウェアの内、以下のものの機能を強化した。

1. NHM変換器： 深さ優先NHM変換に加え、幅優先NHM変換、極小 束縛幅優先(深さ優先)NHM変換機能を実装した。また、モード解析結果によ る冗長節削除機能も加えた。
2. インタプリタ版MGTP： 弁別木プログラムを組み込み、包摂検 査と連言照合に用いることができるようになった。また、連言照合法として RAMS法も導入し、モデル拡張候補集合の実装として、stackかqueueかの指定 ができるようになった。これらの機能は実行時のオプションによりon/offを 指示できる。

○ プログラムサイズとドキュメント

1. プログラムサイズ

   

2. ドキュメント：上記プログラムの各々についてインストール法とコマン ドリファレンスを作成する。また、使用例も掲載する。

(3) 残された課題

推論高速化の点では、弁別木プログラムの開発によりかなりの速度向上が図れ たが、Prologにおける節インデックスに類似の機能を欠くため、入力節数が増 えると場合によっては、推論速度の低下が見られる。節インデックス機能を取 り入れれば、さらなる速度向上が得られるものと考えられる。また、並列KLIC を利用した並列化による速度向上、特に、Folding-up効果を保持しつつ並列化 を計る手法については今後の課題である。

高機能化の点では、探索制御や探索ヒューリスティックといった人工知能にお ける問題解決において、重要な情報を指示できる枠組が今のところMGTPにはな い。今後は、これらを指示できる枠組をMGTPにどのように組み込んでいくかを 検討して行く必要がある。GAを用いたCondensed Detachment問題の取り組みは、 この方向の研究の第一歩であると考えている。

近年GUIシステムは、システムの普及には欠かせないツールとなってきている。 MGTPシステムで、最も開発の遅れているツールはこの部分であると感じている。 特に、証明図描画プログラムは、MGTPの推論過程を直接表示するもので、早急 に作成を行ないたいと考えている。

(4) 評価

本研究は昨年度と今年度の2年計画であり、「可搬性に優れ、使い勝手良いシ ステムを作成する」というのが、当初の目標であった。KLIC上にシステムを構 築した結果、可搬性については、目標を達成したものと考える。また、前処理 部(多数有り)と推論部を一つずつUNIXのコマンドとして作成したので、それら を組み合わせて多様な機能を提供できるようになった。加えてインタプリタ版 の出現により、使い勝手は格段に向上したと実感している。

インタプリタ版MGTP/CMGTPの作成やケース分割の冗長性削除の手法 (Folding-up/down)など、当初の計画にはなかった成果が生まれたことも収穫 であった。