MGTP: A parallel theorem prover based on lazy model generation

Ryuzo Hasegawa; Miyuki Koshimura; Hiroshi Fujita

doi:10.1007/3-540-55602-8_223

MGTP: A parallel theorem prover based on lazy model generation

Ryuzo Hasegawa, Miyuki Koshimura, Hiroshi Fujita

Intelligence Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

3 Citations (Scopus)

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.

Original language	English
Title of host publication	Automated Deduction — CADE-11 - 11 th International Conference on Automated Deduction, Proceedings
Editors	Deepak Kapur
Publisher	Springer Verlag
Pages	776-780
Number of pages	5
ISBN (Print)	9783540556022
DOIs	https://doi.org/10.1007/3-540-55602-8_223
Publication status	Published - 1992
Event	11th International Conference on Automated Deduction, CADE, 1992 - Saratoga Springs, United States Duration: Jun 15 1992 → Jun 18 1992

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	607 LNAI
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Other

Other	11th International Conference on Automated Deduction, CADE, 1992
Country/Territory	United States
City	Saratoga Springs
Period	6/15/92 → 6/18/92

All Science Journal Classification (ASJC) codes

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1007/3-540-55602-8_223

Cite this

Hasegawa, R., Koshimura, M., & Fujita, H. (1992). MGTP: A parallel theorem prover based on lazy model generation. In D. Kapur (Ed.), Automated Deduction — CADE-11 - 11 th International Conference on Automated Deduction, Proceedings (pp. 776-780). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 607 LNAI). Springer Verlag. https://doi.org/10.1007/3-540-55602-8_223

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. ed. / Deepak Kapur. Springer Verlag, 1992. p. 776-780 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 607 LNAI).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Hasegawa, R, Koshimura, M & Fujita, H 1992, MGTP: A parallel theorem prover based on lazy model generation. in D Kapur (ed.), Automated Deduction — CADE-11 - 11 th International Conference on Automated Deduction, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 607 LNAI, Springer Verlag, pp. 776-780, 11th International Conference on Automated Deduction, CADE, 1992, Saratoga Springs, United States, 6/15/92. https://doi.org/10.1007/3-540-55602-8_223

Hasegawa R, Koshimura M, Fujita H. MGTP: A parallel theorem prover based on lazy model generation. In Kapur D, editor, Automated Deduction — CADE-11 - 11 th International Conference on Automated Deduction, Proceedings. Springer Verlag. 1992. p. 776-780. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/3-540-55602-8_223

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. editor / Deepak Kapur. 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",

doi = "10.1007/3-540-55602-8_223",

language = "English",

isbn = "9783540556022",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "776--780",

editor = "Deepak Kapur",

booktitle = "Automated Deduction — CADE-11 - 11 th International Conference on Automated Deduction, Proceedings",

address = "Germany",

note = "11th International Conference on Automated Deduction, CADE, 1992 ; Conference date: 15-06-1992 Through 18-06-1992",

}

TY - GEN

T1 - MGTP

T2 - 11th International Conference on Automated Deduction, CADE, 1992

AU - Hasegawa, Ryuzo

AU - Koshimura, Miyuki

AU - Fujita, Hiroshi

PY - 1992

Y1 - 1992

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

U2 - 10.1007/3-540-55602-8_223

DO - 10.1007/3-540-55602-8_223

M3 - Conference contribution

AN - SCOPUS:85029578900

SN - 9783540556022

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

A2 - Kapur, Deepak

PB - Springer Verlag

Y2 - 15 June 1992 through 18 June 1992

ER -

MGTP: A parallel theorem prover based on lazy model generation

Abstract

Publication series

Other

All Science Journal Classification (ASJC) codes

Access to Document

Other files and links

Fingerprint

Cite this