(11) KLIC上のMGTP処理系

【KLIC上のMGTP処理系の開発研究】

研究代表者：長谷川 隆三 (九州大学大学院システム情報科学研究科 教授)

(１) 研究進捗状況

本研究は，定理証明システムMGTP処理系の高機能化・高速化を計り，操作性や
拡張性，可搬性を高め，広く利用できる魅力あるシステムを作成することを目
的としている．これまでにシステムの中核となる推論部を開発し，定理証明の
ベンチマーク問題を用いた実験を行ってきた．また，探索空間の削減を目的と
したNHM(ノンホーンマジックセット)法やFU(フォールディングアップ)法の効
率的実現手法を検討してきた．

(２) 現在までの主な成果

(ａ) 汎用弁別木プログラムの利用により包摂検査の高速化を図った．

これまでの弁別木プログラムでは，問題に対する前処理の必要があったので，
前処理を行わないインタプリタ版MGTPは，ナイーブな線形検索で包摂検査を行っ
ていた．この点を改良するために，前処理が不要な汎用弁別木プログラムを開
発し，インタプリタ版MGTPに組み込んだ．

(ｂ) NHM法の健全性と完全性の証明を証明図変換の手法を用いて行った．

健全性はNHMの証明からMGTPの証明を作る変換手続きを，完全性は逆の変換手
続きを与えることで示すことができる．これらの変換手続きをKL1で実装し正
当性を検証した．この応用として，証明図変換の手続きで行われる証明図の簡
単化や証明の依存関係の抽出などが，証明図表示や証明の効率化に寄与する見
通しが得られた．

(ｃ) (ｂ)の枠組を利用してFUを実現するMGTPアルゴリズムを考案した． 

本方式は，補題生成によるFU機能による枝刈り効果(ケース分割の冗長性を抑
える)とNHMと類似の冗長性削減効果(ゴールと無関係なモデル候補の拡張を抑
える)の両方を実現する．本方式によるFU付きMGTPを実装しその実験評価行い
良好な結果を得た．

(ｄ) NHM変換のオーバヘッド削減手法を検討した．

一つは，変換によって得られる節数を減らすもの，もう一つは，MGTP推論部の
実装を改善するものである．前者は，修飾子に束構造を導入し，極小な修飾子
のみを用いて変換を行うことにより，節数の増加を抑制する．後者は，変換に
よって得られる付加的な情報goalやcontの照合を，通常のアトムの照合と分離
することで実行効率の向上を行うものである．

(ｅ) Demodulator付きMGTPの簡易版を作成した．本簡易版では方向づけられた等
式を入力節とともに与えることができる．

(３) 今後の研究概要
インタプリタ版制約MGTP(弁別木プログラムを内蔵)を作成し，制約MGTPの利便
性を高め，それを用いて制約充足問題の記述実験を行う．また，GUIをベース
としたMGTPプログラミング環境の開発を行う．Demodulator付きMGTPについて
は，証明中に新たに生成される等号も扱えるように基本アルゴリズムを確立し，
実装する．

新しい試みとして，遺伝的アルゴリズム(GA)を定理証明に組み込む方式の検討
を進めている．これは，証明探索ヒューリスティックとしてGAを利用し効率化
を狙うもので，これまでMGTPで解いてきた問題に適用して，その効果を確かめ
る予定である．

並列化の観点では，分散KLIC上にMGTPを実装し，イーサネット結合した数台規
模のWSを用いて負荷分散実験を行う．また，FD付きMGTPの並列化を行い分散
KLICやPIM上での実験を行う．

(４) 今年度目標成果ソフトウェアイメージ
これまで開発してきた，推論エンジン(MGTPと制約MGTP)と探索空間削減手法
(NHM法，FU法，FD(フォールディングダウン)法)を統合的に利用可能にするGUI
をベースとしたMGTPプログラミング環境を公開する予定である．証明の実行や
結果の表示が基本的にはマウス操作だけで可能になる．