MGTP: A parallel theorem prover based on lazy model generation

研究成果: 著書/レポートタイプへの貢献会議での発言

9 引用 (Scopus)

抄録

We have implemented a model-generation based parallel theorem prover in KL1 on a parallel inference machine, PIM. We have developed several techniques to improve the efficiency of forward reasoning theorem provers based on lazy model generation. The tasks of the model-generation based prover are the generation and testing of atoms to be the elements of a model for the given theorem. The problem with this method is the explosion in the number of generated atoms and in the computational cost in time and space, incurred by the generation processes. Lazy model generation is a new method that avoids the generation of unnecessary atoms that are irrelevant to obtaining proofs, and to provide flexible control for the efficient use of resources in a parallel environment. With this method we have achieved a more than one-hundred-fold speedup on a PIM consisting of 128 PEs.

元の言語英語
ホスト出版物のタイトルAutomated Deduction — CADE-11 - 11 th International Conference on Automated Deduction, Proceedings
出版者Springer Verlag
ページ776-780
ページ数5
607 LNAI
ISBN(印刷物)9783540556022
出版物ステータス出版済み - 1 1 1992
外部発表Yes
イベント11th International Conference on Automated Deduction, CADE, 1992 - Saratoga Springs, 米国
継続期間: 6 15 19926 18 1992

出版物シリーズ

名前Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
607 LNAI
ISSN(印刷物)0302-9743
ISSN(電子版)1611-3349

その他

その他11th International Conference on Automated Deduction, CADE, 1992
米国
Saratoga Springs
期間6/15/926/18/92

Fingerprint

Theorem
Atoms
Model
Explosions
Explosion
Computational Cost
Speedup
Fold
Reasoning
Testing
Costs
Resources

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

これを引用

Hasegawa, R., Koshimura, M., & Fujita, H. (1992). MGTP: A parallel theorem prover based on lazy model generation. : Automated Deduction — CADE-11 - 11 th International Conference on Automated Deduction, Proceedings (巻 607 LNAI, pp. 776-780). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); 巻数 607 LNAI). Springer Verlag.

MGTP : A parallel theorem prover based on lazy model generation. / Hasegawa, Ryuzo; Koshimura, Miyuki; Fujita, Hiroshi.

Automated Deduction — CADE-11 - 11 th International Conference on Automated Deduction, Proceedings. 巻 607 LNAI Springer Verlag, 1992. p. 776-780 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); 巻 607 LNAI).

研究成果: 著書/レポートタイプへの貢献会議での発言

Hasegawa, R, Koshimura, M & Fujita, H 1992, MGTP: A parallel theorem prover based on lazy model generation. : Automated Deduction — CADE-11 - 11 th International Conference on Automated Deduction, Proceedings. 巻. 607 LNAI, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 巻. 607 LNAI, Springer Verlag, pp. 776-780, 11th International Conference on Automated Deduction, CADE, 1992, Saratoga Springs, 米国, 6/15/92.
Hasegawa R, Koshimura M, Fujita H. MGTP: A parallel theorem prover based on lazy model generation. : Automated Deduction — CADE-11 - 11 th International Conference on Automated Deduction, Proceedings. 巻 607 LNAI. Springer Verlag. 1992. p. 776-780. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
Hasegawa, Ryuzo ; Koshimura, Miyuki ; Fujita, Hiroshi. / MGTP : A parallel theorem prover based on lazy model generation. Automated Deduction — CADE-11 - 11 th International Conference on Automated Deduction, Proceedings. 巻 607 LNAI Springer Verlag, 1992. pp. 776-780 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{1d75f1dfb3574f3c87a6f91acdf15cec,
title = "MGTP: A parallel theorem prover based on lazy model generation",
abstract = "We have implemented a model-generation based parallel theorem prover in KL1 on a parallel inference machine, PIM. We have developed several techniques to improve the efficiency of forward reasoning theorem provers based on lazy model generation. The tasks of the model-generation based prover are the generation and testing of atoms to be the elements of a model for the given theorem. The problem with this method is the explosion in the number of generated atoms and in the computational cost in time and space, incurred by the generation processes. Lazy model generation is a new method that avoids the generation of unnecessary atoms that are irrelevant to obtaining proofs, and to provide flexible control for the efficient use of resources in a parallel environment. With this method we have achieved a more than one-hundred-fold speedup on a PIM consisting of 128 PEs.",
author = "Ryuzo Hasegawa and Miyuki Koshimura and Hiroshi Fujita",
year = "1992",
month = "1",
day = "1",
language = "English",
isbn = "9783540556022",
volume = "607 LNAI",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "776--780",
booktitle = "Automated Deduction — CADE-11 - 11 th International Conference on Automated Deduction, Proceedings",
address = "Germany",

}

TY - GEN

T1 - MGTP

T2 - A parallel theorem prover based on lazy model generation

AU - Hasegawa, Ryuzo

AU - Koshimura, Miyuki

AU - Fujita, Hiroshi

PY - 1992/1/1

Y1 - 1992/1/1

N2 - We have implemented a model-generation based parallel theorem prover in KL1 on a parallel inference machine, PIM. We have developed several techniques to improve the efficiency of forward reasoning theorem provers based on lazy model generation. The tasks of the model-generation based prover are the generation and testing of atoms to be the elements of a model for the given theorem. The problem with this method is the explosion in the number of generated atoms and in the computational cost in time and space, incurred by the generation processes. Lazy model generation is a new method that avoids the generation of unnecessary atoms that are irrelevant to obtaining proofs, and to provide flexible control for the efficient use of resources in a parallel environment. With this method we have achieved a more than one-hundred-fold speedup on a PIM consisting of 128 PEs.

AB - We have implemented a model-generation based parallel theorem prover in KL1 on a parallel inference machine, PIM. We have developed several techniques to improve the efficiency of forward reasoning theorem provers based on lazy model generation. The tasks of the model-generation based prover are the generation and testing of atoms to be the elements of a model for the given theorem. The problem with this method is the explosion in the number of generated atoms and in the computational cost in time and space, incurred by the generation processes. Lazy model generation is a new method that avoids the generation of unnecessary atoms that are irrelevant to obtaining proofs, and to provide flexible control for the efficient use of resources in a parallel environment. With this method we have achieved a more than one-hundred-fold speedup on a PIM consisting of 128 PEs.

UR - http://www.scopus.com/inward/record.url?scp=85029578900&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85029578900&partnerID=8YFLogxK

M3 - Conference contribution

AN - SCOPUS:85029578900

SN - 9783540556022

VL - 607 LNAI

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 776

EP - 780

BT - Automated Deduction — CADE-11 - 11 th International Conference on Automated Deduction, Proceedings

PB - Springer Verlag

ER -