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

Ryuzo Hasegawa, Katsumi Inoue, Yoshihiko Ohta, Miyuki Koshimura

研究成果: Chapter in Book/Report/Conference proceedingConference contribution

19 被引用数 (Scopus)

抄録

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.

本文言語英語
ホスト出版物のタイトルAutomated Deduction – CADE-14 - 14th International Conference on Automated Deduction, Proceedings
編集者William McCune
出版社Springer Verlag
ページ176-190
ページ数15
ISBN(印刷版)3540631046, 9783540631040
DOI
出版ステータス出版済み - 1997
イベント14th International Conference on Automated Deduction, CADE 1997 - Townsville, オーストラリア
継続期間: 7 13 19977 17 1997

出版物シリーズ

名前Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
1249
ISSN(印刷版)0302-9743
ISSN(電子版)1611-3349

その他

その他14th International Conference on Automated Deduction, CADE 1997
Countryオーストラリア
CityTownsville
Period7/13/977/17/97

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

フィンガープリント 「Non-horn magic sets to incorporate top-down inference into bottom-up theorem proving」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル