Building a Distributed Knowledge Information System Based on Model Generation

构建基于模型生成的分布式知识信息系统

• 批准号: 08458080
• 负责人: HASEGAWA Ryuzo
• 金额: $ 3.65万
• 依托单位: KYUSHU UNIVERSITY
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (B)
• 财政年份: 1996
• 资助国家: 日本
• 起止时间: 1996 至 1998
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-08458080/
• 关键词: Model Generation; NHM Method; Folding-up Method; Java Language; OR-Parallelization; N-Sequential Method; Constraint Processing; Search Control; N逐次実行方式; Folding-up機能; 多重環境; 項インデキシング; 並列探索; Java; 異機種分散; モデル生成; 定理証明; 弁別木プログラム; 並列処理; 知識情報処

We have developed a parallel model-generation based theorem-proving system MGTP with novel techniques for efficient proof-search and successful applications.We have also developed CMGTP (Constraint MGTP) to deal with constraint satisfaction problems. By attaining the constraint propagation with negative atoms, CMGTP makes it possible to reduce search spaces by orders of magnitude compared to the original MGTP.To enhance the ability to prune search spaces, we have developed a new method called non-Horn magic sets (NHM) and incorporated its relevancy testing function into the folding-up (FU) method proposed by Letz. The NHM method suppresses useless model generation with clauses irrelevant to the goal. The FU method avoids generating duplicated subproofs after case-splitting. With these methods we can eliminate two major kinds of redundancies in model-generation based theorem provers.An efficient parallel execution method is presented for parallel programs which create many tasks at runtime on parallel machines with N number of processing elements (PEs) available at any time. In this method, the number of tasks activated at the same time is limited to at most N, and the exceeding number of created tasks are suspended until they are allowed to be activated, thus being processed sequentially. We implemented the method for the parallel theorem proving system MGTP written in the concurrent programming language KL1 running on the parallel inference machine PIM/m (128PE) as well as the shared-memory parallel machine Cray SuperServer6400 (20PE). The results show remarkable reduction of communication overhead achieving significant speedup.We have studied heuristic proof-search based on the genetic algorithm.

我们已经开发了一种基于平行模型产生的定理系统MGTP，它采用了新颖的技术来进行有效的证明和成功应用程序。我们还开发了CMGTP（约束MGTP）来处理约束满意度问题。通过使用负原子进行约束传播，CMGTP可以通过与原始MGTP相比，通过数量级来减少搜索空间，以增强修剪搜索空间的能力，我们开发了一种称为非Horn Magic Sets（NHM）的新方法，并将其相关测试函数纳入折叠功能（FU）方法。 NHM方法抑制了与目标无关的条款无用的模型生成。 FU方法避免在拆分案例后产生重复的子设备。通过这些方法，我们可以在基于模型生成的定理掠夺中消除两种主要的裁员。为并行程序提供了有效的并行执行方法，这些方法在任何时间可用的并行机器上在并行机器上创建许多任务。在这种方法中，同时激活的任务数量最多仅限于N，并且超过创建的任务数量被暂停，直到允许它们被激活为止，从而被依次处理。我们实施了以并行编程语言KL1编写的并行推理计算机PIM/M（128pe）以及共享 - 内存的平行机cray superserver6400（20pe）的同时编程语言KL1编写的方法MGTP MGTP。结果表明，沟通高架的速度显着降低，从而实现了显着的加速。我们研究了基于遗传算法的启发式证明搜索。

项目成果

Ryuzo Hasegawa, Hiroshi Fujita and Miyuki Koshimura: " MGTP : A Parallel Theorem-Proving Sys-tem Based on Model Generation" In Proc.11th Intl.Conf.on Applications of Prolog. 34-41 (1998)

Ryuzo Hasekawa、Hiroshi Fujita 和 Miyuki Koshimura：“MGTP：基于模型生成的并行定理证明系统”，Proc.11th Intl.Conf.on 应用 Prolog。

白井.長谷川: "モデル生成型定理証明システムによる制約充足問題の解決とその並列化" 電子情報通信学会論文誌. J80 D-II 1. 224-236 (1997)

Hasekawa, Shirai：“使用模型生成定理证明系统及其并行化解决约束满足问题”，电子、信息和通信工程师学会汇刊 J80 D-II 1. 224-236 (1997)。

長谷川隆三,藤田博: "制約問題を解くためのモデル生成型定理証明系の新実装法" 九州大学大学院システム情報科学研究科報告. 4・1(印刷中). (1999)

Ryuzo Hasekawa、Hiroshi Fujita：“解决约束问题的模型生成定理证明系统的新实现方法”九州大学系统与信息科学研究生院报告4/1（出版中）。

藤田.長谷川.: "Java言語によるモデル生成型定理証明系MGTPの実装" 九州大学大学院システム情報科学研究科報告. 3・1. 63-68 (1998)

藤田.长谷川：“使用Java语言实现模型生成型定理证明系统MGTP”九州大学系统与信息科学研究生院报告3·1（1998）。

Ryuzo Hasegawa, Katsumi Inoue, Yoshihiko Ohta and Miyuki Koshimura: "Non-Horn Magic Sets to Incorporate Top-down Inference into Bottom-up Theorem Proving" In Proc.Intl.Conf.on Automated Deduction, Lecture Notes in Artificial Intelligence, Springer-Verlag.

Ryuzo Hasekawa、Katsumi Inoue、Yoshihiko Ohta 和 Miyuki Koshimura：“Non-Horn Magic Sets to Incorporated Top-down Inference into Bottom-up Theorem Proving” In Proc.Intl.Conf.on Automated Deduction，人工智能讲义，Springer-