MGTP: A model generation theorem prover-its advanced features and applications

Ryuzo Hasegawa, Hiroshi Fujita, Miyuki Koshimura

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

9 Citations (Scopus)


This paper outlines a parallel model-generation based theoremproving system MGTP that we have been developing, focusing on the recent developments including novel techniques for efficient proof-search and successful applications. We have 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. We have studied several applications in AI such as negation as failure, abductive reasoning and modal logic systems, through extensive use of MGTP. These studies share a basic common idea, that is, to use MGTP as a meta-programming system. We can build various reasoning systems on MGTP by writing the specific inference rules for each system in MGTP input clauses. Furthermore, we are now working on other applications such as machine learning with MGTP and heuristic proof-search based on the genetic algorithm.

Original languageEnglish
Title of host publicationAutomated Reasoning with Analytic Tableaux and Related Methods - International Conference, TABLEAUX 1997, Proceedings
EditorsDidier Galmiche
PublisherSpringer Verlag
Number of pages15
ISBN (Print)3540629203, 9783540629207
Publication statusPublished - 1997
EventInternational Conference on Analytic Tableaux and Related Methods, TABLEAUX 1997 - Pont-a-Mousson, France
Duration: May 13 1997May 16 1997

Publication series

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


OtherInternational Conference on Analytic Tableaux and Related Methods, TABLEAUX 1997

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'MGTP: A model generation theorem prover-its advanced features and applications'. Together they form a unique fingerprint.

Cite this