Embedding delayed relevancy testing and folding-up into CMGTP

Tsuyoshi Tatebayashi, Miyuki Koshimura, Ryuzo Hasegawa

Research output: Contribution to journalArticlepeer-review

1 Citation (Scopus)


We present a method embedding two mechanisms, which eliminate redundant inferences, into CMGTP. One is delayed relevancy testing which eliminates unnecessary subproofs by calculating relevancy to the proof. Another is folding-up which eliminates a duplicate subproof by using lemmas extracted from the proof. These two mechanisms are achieved by extracting literals that have contributed to the proof. We have implemented the method in Java and evaluated its effects for some typical problems taken from the TPTP problem library.

Original languageEnglish
Pages (from-to)151-158
Number of pages8
JournalResearch Reports on Information Science and Electrical Engineering of Kyushu University
Issue number2
Publication statusPublished - Sept 1999

All Science Journal Classification (ASJC) codes

  • General Computer Science
  • Electrical and Electronic Engineering


Dive into the research topics of 'Embedding delayed relevancy testing and folding-up into CMGTP'. Together they form a unique fingerprint.

Cite this