Non-horn magic sets to incorporate top-down inference into bottom-up theorem proving

Ryuzo Hasegawa, Katsumi Inoue, Yoshihiko Ohta, Miyuki Koshimura

Research output: Chapter in Book/Report/Conference proceedingConference contribution

19 Citations (Scopus)

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 atoms of an original clause in parallel. The second one evaluates them sequentially while propagating the bindings in an antecedent atom 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 effects of NHM by proving some typical problems taken from the TPTP problem library.

Original languageEnglish
Title of host publicationAutomated Deduction – CADE-14 - 14th International Conference on Automated Deduction, Proceedings
PublisherSpringer Verlag
Pages176-190
Number of pages15
Volume1249
ISBN (Print)3540631046, 9783540631040
Publication statusPublished - Jan 1 1997
Event14th International Conference on Automated Deduction, CADE 1997 - Townsville, Australia
Duration: Jul 13 1997Jul 17 1997

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1249
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other14th International Conference on Automated Deduction, CADE 1997
CountryAustralia
CityTownsville
Period7/13/977/17/97

Fingerprint

Theorem proving
Theorem Proving
Bottom-up
Atoms
UNIX
Acoustic waves
Breadth
Evaluate
Natural Extension
Predicate
Continuation
Reasoning

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Hasegawa, R., Inoue, K., Ohta, Y., & Koshimura, M. (1997). Non-horn magic sets to incorporate top-down inference into bottom-up theorem proving. In Automated Deduction – CADE-14 - 14th International Conference on Automated Deduction, Proceedings (Vol. 1249, pp. 176-190). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1249). Springer Verlag.

Non-horn magic sets to incorporate top-down inference into bottom-up theorem proving. / Hasegawa, Ryuzo; Inoue, Katsumi; Ohta, Yoshihiko; Koshimura, Miyuki.

Automated Deduction – CADE-14 - 14th International Conference on Automated Deduction, Proceedings. Vol. 1249 Springer Verlag, 1997. p. 176-190 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1249).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Hasegawa, R, Inoue, K, Ohta, Y & Koshimura, M 1997, Non-horn magic sets to incorporate top-down inference into bottom-up theorem proving. in Automated Deduction – CADE-14 - 14th International Conference on Automated Deduction, Proceedings. vol. 1249, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 1249, Springer Verlag, pp. 176-190, 14th International Conference on Automated Deduction, CADE 1997, Townsville, Australia, 7/13/97.
Hasegawa R, Inoue K, Ohta Y, Koshimura M. Non-horn magic sets to incorporate top-down inference into bottom-up theorem proving. In Automated Deduction – CADE-14 - 14th International Conference on Automated Deduction, Proceedings. Vol. 1249. Springer Verlag. 1997. p. 176-190. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
Hasegawa, Ryuzo ; Inoue, Katsumi ; Ohta, Yoshihiko ; Koshimura, Miyuki. / Non-horn magic sets to incorporate top-down inference into bottom-up theorem proving. Automated Deduction – CADE-14 - 14th International Conference on Automated Deduction, Proceedings. Vol. 1249 Springer Verlag, 1997. pp. 176-190 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{7f0c5007d7204c4ab153f891f67f4766,
title = "Non-horn magic sets to incorporate top-down inference into 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 atoms of an original clause in parallel. The second one evaluates them sequentially while propagating the bindings in an antecedent atom 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 effects of NHM by proving some typical problems taken from the TPTP problem library.",
author = "Ryuzo Hasegawa and Katsumi Inoue and Yoshihiko Ohta and Miyuki Koshimura",
year = "1997",
month = "1",
day = "1",
language = "English",
isbn = "3540631046",
volume = "1249",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "176--190",
booktitle = "Automated Deduction – CADE-14 - 14th International Conference on Automated Deduction, Proceedings",
address = "Germany",

}

TY - GEN

T1 - Non-horn magic sets to incorporate top-down inference into bottom-up theorem proving

AU - Hasegawa, Ryuzo

AU - Inoue, Katsumi

AU - Ohta, Yoshihiko

AU - Koshimura, Miyuki

PY - 1997/1/1

Y1 - 1997/1/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 atoms of an original clause in parallel. The second one evaluates them sequentially while propagating the bindings in an antecedent atom 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 effects of NHM 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 atoms of an original clause in parallel. The second one evaluates them sequentially while propagating the bindings in an antecedent atom 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 effects of NHM by proving some typical problems taken from the TPTP problem library.

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

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

M3 - Conference contribution

SN - 3540631046

SN - 9783540631040

VL - 1249

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 176

EP - 190

BT - Automated Deduction – CADE-14 - 14th International Conference on Automated Deduction, Proceedings

PB - Springer Verlag

ER -