MGTP: A parallel theorem prover based on lazy model generation

Ryuzo Hasegawa, Miyuki Koshimura, Hiroshi Fujita

Research output: Chapter in Book/Report/Conference proceedingConference contribution

9 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 languageEnglish
Title of host publicationAutomated Deduction — CADE-11 - 11 th International Conference on Automated Deduction, Proceedings
EditorsDeepak Kapur
PublisherSpringer Verlag
Pages776-780
Number of pages5
ISBN (Print)9783540556022
DOIs
Publication statusPublished - 1992
Event11th International Conference on Automated Deduction, CADE, 1992 - Saratoga Springs, United States
Duration: Jun 15 1992Jun 18 1992

Publication series

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

Other

Other11th International Conference on Automated Deduction, CADE, 1992
CountryUnited States
CitySaratoga Springs
Period6/15/926/18/92

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'MGTP: A parallel theorem prover based on lazy model generation'. Together they form a unique fingerprint.

  • 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