Embedding delayed relevancy testing and folding-up into CMGTP

Tsuyoshi Tatebayashi, Miyuki Koshimura, Ryuzo Hasegawa

Research output: Contribution to journalArticle

1 Citation (Scopus)

Abstract

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
Volume4
Issue number2
Publication statusPublished - Sep 1999

All Science Journal Classification (ASJC) codes

  • Hardware and Architecture
  • Engineering (miscellaneous)
  • Electrical and Electronic Engineering

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

  • Cite this