| Project/Area Number |
08458080
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
Intelligent informatics
|
|---|
| Research Institution | KYUSHU UNIVERSITY |
|---|
Principal Investigator |
HASEGAWA Ryuzo Graduate School of Information Science and Electrical Engineering, KYUSHU UNIVERSITY,Professor, 大学院・システム情報科学研究科, 教授 (20274483)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
KOSHIMURA Miyuki Graduate School of Information Science and Electrical Engineering, KYUSHU UNIVER, 大学院・システム情報科学研究科, 助手 (30274492)
FUJITA Hiroshi Graduate School of Information Science and Electrical Engineering, KYUSHU UNIVER, 大学院・システム情報科学研究科, 助教授 (70284552)
|
|---|
| Project Period (FY) |
1996 – 1998
|
| Project Status |
Completed (Fiscal Year 1998)
|
| Budget Amount *help |
¥5,700,000 (Direct Cost: ¥5,700,000)
Fiscal Year 1998: ¥800,000 (Direct Cost: ¥800,000)
Fiscal Year 1997: ¥2,700,000 (Direct Cost: ¥2,700,000)
Fiscal Year 1996: ¥2,200,000 (Direct Cost: ¥2,200,000)
|
|---|
| Keywords | Model Generation / NHM Method / Folding-up Method / Java Language / OR-Parallelization / N-Sequential Method / Constraint Processing / Search Control / N逐次実行方式 / Folding-up機能 / 多重環境 / 項インデキシング / 並列探索 / Java / 異機種分散 / モデル生成 / 定理証明 / 弁別木プログラム / 並列処理 / 知識情報処理 |
|---|
| Research Abstract |
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.
|
