A method to eliminate redundant case-splittings in MGTP and its evaluation

Takashi Matsumoto, Miyuki Koshimura, Tetsuji Kuboyama, Ryuzo Hasegawa

研究成果: Contribution to journalArticle査読


We present a new method to eliminate redundant inferences caused by case-splitting in MGTP. There are two types of redundancies eliminated by the method: One is that the same sub-proof tree may be generated at several descendant nodes after a case-splitting occurs. Another is caused by useless model candidate extensions with irrelevant non-Horn clauses. Both types of redundancies can be eliminated by combining the folding-up function that conveys unit lemmata obtained from solved descendant nodes to a proper antecedent node and the NHM function that suppresses useless model extensions. The method has been implemented in MGTP. We evaluate its effects on a UNIX workstation for some typical problems taken from the TPTP problem library.

ジャーナルResearch Reports on Information Science and Electrical Engineering of Kyushu University
出版ステータス出版済み - 3 1 1997

All Science Journal Classification (ASJC) codes

  • コンピュータ サイエンス(全般)
  • 電子工学および電気工学


「A method to eliminate redundant case-splittings in MGTP and its evaluation」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。