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

Ryuzo Hasegawa, Hiroshi Fujita, Miyuki Koshimura

研究成果: Chapter in Book/Report/Conference proceedingConference contribution

8 被引用数 (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.

本文言語英語
ホスト出版物のタイトルAutomated Reasoning with Analytic Tableaux and Related Methods - International Conference, TABLEAUX 1997, Proceedings
編集者Didier Galmiche
出版社Springer Verlag
ページ1-15
ページ数15
ISBN(印刷版)3540629203, 9783540629207
DOI
出版ステータス出版済み - 1997
イベントInternational Conference on Analytic Tableaux and Related Methods, TABLEAUX 1997 - Pont-a-Mousson, フランス
継続期間: 5 13 19975 16 1997

出版物シリーズ

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

その他

その他International Conference on Analytic Tableaux and Related Methods, TABLEAUX 1997
Countryフランス
CityPont-a-Mousson
Period5/13/975/16/97

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

フィンガープリント 「MGTP: A model generation theorem prover-its advanced features and applications」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル