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

Takashi Matsumoto, Miyuki Koshimura, Tetsuji Kuboyama, Ryuzo Hasegawa

Research output: Contribution to journalArticle

Abstract

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.

Original languageEnglish
Pages (from-to)75-80
Number of pages6
JournalResearch Reports on Information Science and Electrical Engineering of Kyushu University
Volume2
Issue number1
Publication statusPublished - Mar 1997

Fingerprint

Redundancy
UNIX

All Science Journal Classification (ASJC) codes

  • Computer Science(all)
  • Electrical and Electronic Engineering

Cite this

A method to eliminate redundant case-splittings in MGTP and its evaluation. / Matsumoto, Takashi; Koshimura, Miyuki; Kuboyama, Tetsuji; Hasegawa, Ryuzo.

In: Research Reports on Information Science and Electrical Engineering of Kyushu University, Vol. 2, No. 1, 03.1997, p. 75-80.

Research output: Contribution to journalArticle

@article{6d587342cf40462fb2a75c31b316d1fd,
title = "A method to eliminate redundant case-splittings in MGTP and its evaluation",
abstract = "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.",
author = "Takashi Matsumoto and Miyuki Koshimura and Tetsuji Kuboyama and Ryuzo Hasegawa",
year = "1997",
month = "3",
language = "English",
volume = "2",
pages = "75--80",
journal = "Research Reports on Information Science and Electrical Engineering of Kyushu University",
issn = "1342-3819",
publisher = "Kyushu University, Faculty of Science",
number = "1",

}

TY - JOUR

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

AU - Matsumoto, Takashi

AU - Koshimura, Miyuki

AU - Kuboyama, Tetsuji

AU - Hasegawa, Ryuzo

PY - 1997/3

Y1 - 1997/3

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

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

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

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

M3 - Article

VL - 2

SP - 75

EP - 80

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 - 1

ER -