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

Fingerprint

Testing

All Science Journal Classification (ASJC) codes

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

Cite this

Embedding delayed relevancy testing and folding-up into CMGTP. / Tatebayashi, Tsuyoshi; Koshimura, Miyuki; Hasegawa, Ryuzo.

In: Research Reports on Information Science and Electrical Engineering of Kyushu University, Vol. 4, No. 2, 09.1999, p. 151-158.

Research output: Contribution to journalArticle

@article{4488d95b192047f2bc660c784b161631,
title = "Embedding delayed relevancy testing and folding-up into CMGTP",
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.",
author = "Tsuyoshi Tatebayashi and Miyuki Koshimura and Ryuzo Hasegawa",
year = "1999",
month = "9",
language = "English",
volume = "4",
pages = "151--158",
journal = "Research Reports on Information Science and Electrical Engineering of Kyushu University",
issn = "1342-3819",
publisher = "Kyushu University, Faculty of Science",
number = "2",

}

TY - JOUR

T1 - Embedding delayed relevancy testing and folding-up into CMGTP

AU - Tatebayashi, Tsuyoshi

AU - Koshimura, Miyuki

AU - Hasegawa, Ryuzo

PY - 1999/9

Y1 - 1999/9

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=0033341838&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0033341838&partnerID=8YFLogxK

M3 - Article

AN - SCOPUS:0033341838

VL - 4

SP - 151

EP - 158

JO - Research Reports on Information Science and Electrical Engineering of Kyushu University

JF - Research Reports on Information Science and Electrical Engineering of Kyushu University

SN - 1342-3819

IS - 2

ER -