Non-Horn magic sets for bottom-up theorem proving

Ryuzo Hasegawa, Miyuki Koshimura, Katsumi Inoue, Yoshihiko Ohta

研究成果: ジャーナルへの寄稿記事

抄録

We present a new method, called non-Horn magic sets(NHM), to enhance forward reasoning provers by combining top-down and bottom-up computations. This method is a natural extension of Horn magic sets and is applicable to range-restricted non-Horn clauses. We show two types of transformations to get non-Horn magic sets from the given clause sets: breadth-first NHM and depth-first NHM. The first transformation evaluates the antecedent literals of a transformed clause in parallel. The second one evaluates them sequentially while propagating the bindings in an antecedent literal to the next by using continuation predicates. These transformations are shown to be sound and complete. The NHM method has been implemented on a UNIX workstation. We evaluated NHM effects by proving some typical problems taken from the TPTP problem library.

元の言語英語
ページ(範囲)85-90
ページ数6
ジャーナルResearch Reports on Information Science and Electrical Engineering of Kyushu University
1
発行部数1
出版物ステータス出版済み - 9 1 1996

Fingerprint

Theorem proving
UNIX
Acoustic waves

All Science Journal Classification (ASJC) codes

  • Computer Science(all)
  • Electrical and Electronic Engineering

これを引用

Non-Horn magic sets for bottom-up theorem proving. / Hasegawa, Ryuzo; Koshimura, Miyuki; Inoue, Katsumi; Ohta, Yoshihiko.

:: Research Reports on Information Science and Electrical Engineering of Kyushu University, 巻 1, 番号 1, 01.09.1996, p. 85-90.

研究成果: ジャーナルへの寄稿記事

@article{89dd11b6e2014a50ad3b2075120fea78,
title = "Non-Horn magic sets for bottom-up theorem proving",
abstract = "We present a new method, called non-Horn magic sets(NHM), to enhance forward reasoning provers by combining top-down and bottom-up computations. This method is a natural extension of Horn magic sets and is applicable to range-restricted non-Horn clauses. We show two types of transformations to get non-Horn magic sets from the given clause sets: breadth-first NHM and depth-first NHM. The first transformation evaluates the antecedent literals of a transformed clause in parallel. The second one evaluates them sequentially while propagating the bindings in an antecedent literal to the next by using continuation predicates. These transformations are shown to be sound and complete. The NHM method has been implemented on a UNIX workstation. We evaluated NHM effects by proving some typical problems taken from the TPTP problem library.",
author = "Ryuzo Hasegawa and Miyuki Koshimura and Katsumi Inoue and Yoshihiko Ohta",
year = "1996",
month = "9",
day = "1",
language = "English",
volume = "1",
pages = "85--90",
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 - Non-Horn magic sets for bottom-up theorem proving

AU - Hasegawa, Ryuzo

AU - Koshimura, Miyuki

AU - Inoue, Katsumi

AU - Ohta, Yoshihiko

PY - 1996/9/1

Y1 - 1996/9/1

N2 - We present a new method, called non-Horn magic sets(NHM), to enhance forward reasoning provers by combining top-down and bottom-up computations. This method is a natural extension of Horn magic sets and is applicable to range-restricted non-Horn clauses. We show two types of transformations to get non-Horn magic sets from the given clause sets: breadth-first NHM and depth-first NHM. The first transformation evaluates the antecedent literals of a transformed clause in parallel. The second one evaluates them sequentially while propagating the bindings in an antecedent literal to the next by using continuation predicates. These transformations are shown to be sound and complete. The NHM method has been implemented on a UNIX workstation. We evaluated NHM effects by proving some typical problems taken from the TPTP problem library.

AB - We present a new method, called non-Horn magic sets(NHM), to enhance forward reasoning provers by combining top-down and bottom-up computations. This method is a natural extension of Horn magic sets and is applicable to range-restricted non-Horn clauses. We show two types of transformations to get non-Horn magic sets from the given clause sets: breadth-first NHM and depth-first NHM. The first transformation evaluates the antecedent literals of a transformed clause in parallel. The second one evaluates them sequentially while propagating the bindings in an antecedent literal to the next by using continuation predicates. These transformations are shown to be sound and complete. The NHM method has been implemented on a UNIX workstation. We evaluated NHM effects by proving some typical problems taken from the TPTP problem library.

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

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

M3 - Article

AN - SCOPUS:0030233829

VL - 1

SP - 85

EP - 90

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 -