モデル生成型定理証明に基づく分散知識情報処理システムの構築

1998 Fiscal Year Annual Research Report

• Project/Area Number: 08458080
• Research Institution: KYUSHU UNIVERSITY
• Principal Investigator: 長谷川 隆三 九州大学, 大学院システム情報科学研究所, 教授 (20274483)
• Co-Investigator(Kenkyū-buntansha): 越村 三幸 九州大学, 大学院システム情報科学研究所, 助手 (30274492) ; 藤田 博 九州大学, 大学院システム情報科学研究所, 助教授 (70284552)
• Keywords: N逐次実行方式 / Folding-up機能 / 多重環境 / 項インデキシング / 並列探索

Research Abstract

本年度は、(1)N逐次実行方式によるFolding-up付きMGTPの並列化とその評価、及び(2)Java-CMGTPの効率化技法の検討と評価、を行った。(1)は、深さ優先探索で真価を発揮する枝刈り手法(Folding-up)の能力をできるだけ落さない並列化手法、(2)は、多重環境の効率的実装法、の確立を狙った研究である。
1. N逐次実行方式によるFolding-up付きMGTPの並列化:本来逐次処理に向いていると考えられている、関連性テスト付きfolding-up機能を持つMGTPを、既にMGTPの並列化に高い効果を上げているN逐次実行方式を用いて並列化し、それによる証明時間の短縮の可能性について評価を行い、次の結論を得た。
●並列実行した場合、その性質上冗長な探索を行ってしまうため、証明時間がPE台数に比例するような台数効果を得ることは難しい。しかしながら、問題によってはある程度の効果を得られる。
●逐次アルゴリズムでは永久に探索を行ってしまうような場合についても、それが冗長な探索である場合には、並列探索を利用して他PEによる枝刈りを行わせ、その効果を確認した。
2. Java-CMGTPの効率化技法の検討と評価:JavaによるCMGTPの実装において、以下の実装技法が、従来のCMGTP処理系に比べて大きな性能改善をもたらすことが判明した。
●複製によらない多重環境の実現
●Activation-cellによるO(1)時間所属検査
●多重環境下での効果的な項インデキシング機構

Research Products

• [Publications] 藤田博,長谷川隆三: "Jara言語によるモデル生成型定理証明系MGTPの実装" 九州大学大学院システム情報科学研究科報告. 3・1. 63-68 (1998)
• [Publications] 長谷川隆三,藤田博: "制約問題を解くためのモデル生成型定理証明系の新実装法" 九州大学大学院システム情報科学研究科報告. 4・1(印刷中). (1999)