WEKO3
アイテム
上昇型定理証明の探索効率を高めるノンホーン・マジックセット
https://ipsj.ixsq.nii.ac.jp/records/13449
https://ipsj.ixsq.nii.ac.jp/records/134490342dab8-8511-4553-9fbd-25cc0a07ed93
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-JNL3803008.pdf (1.2 MB)
|
Copyright (c) 1997 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | Journal(1) | |||||||
|---|---|---|---|---|---|---|---|---|
| 公開日 | 1997-03-15 | |||||||
| タイトル | ||||||||
| タイトル | 上昇型定理証明の探索効率を高めるノンホーン・マジックセット | |||||||
| タイトル | ||||||||
| 言語 | en | |||||||
| タイトル | Non - Horn Magic Sets to Enhance the Search Efficiency of Botton-up Theorem Proving | |||||||
| 言語 | ||||||||
| 言語 | jpn | |||||||
| キーワード | ||||||||
| 主題Scheme | Other | |||||||
| 主題 | 論文 | |||||||
| 資源タイプ | ||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_6501 | |||||||
| 資源タイプ | journal article | |||||||
| その他タイトル | ||||||||
| その他のタイトル | 知識処理 | |||||||
| 著者所属 | ||||||||
| 九州大学大学院システム情報科学研究科 | ||||||||
| 著者所属 | ||||||||
| 豊橋技術科学大学情報工学系 | ||||||||
| 著者所属 | ||||||||
| 職業能力開発大学校情報工学科 | ||||||||
| 著者所属 | ||||||||
| 九州大学大学院システム情報科学研究科 | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Kyushu University | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Toyohashi University of Technology | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| University of Industrial Technology | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Kyushu University | ||||||||
| 著者名 |
長谷川, 隆三
× 長谷川, 隆三
|
|||||||
| 著者名(英) |
Ryuzo, Hasegawa
× Ryuzo, Hasegawa
|
|||||||
| 論文抄録 | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | 本論文では，上昇型および下降型計算を融合することにより，前向き推論に基づく定理証明器の効率を改善する，ノンホーン・マジックセット（NHM）と呼ぶ新しい方法を提案する．本方法は，ホーン節集合に対するマジックセット法の自然な拡張となっており，値域限定されたノンホーン節に適用可能である．与えられた節集合からNHMを得る方式として，幅優先NHMおよび深さ優先NHMの2種の変換方式を提示する．前者は変換前の元の節の前件アトムを並列に評価し，一方後者は，継続述語により変数束縛情報を伝播しながら前件アトムを逐次的に評価する．そして，両変換方式は健全かつ完全であることを示す．NHM法をUNIXワークステーション上に実装し，定理証明の典型的ベンチマーク問題を対象にその有効性を確認した． | |||||||
| 論文抄録(英) | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | 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. | |||||||
| 書誌レコードID | ||||||||
| 収録物識別子タイプ | NCID | |||||||
| 収録物識別子 | AN00116647 | |||||||
| 書誌情報 |
情報処理学会論文誌 巻 38, 号 3, p. 453-461, 発行日 1997-03-15 |
|||||||
| ISSN | ||||||||
| 収録物識別子タイプ | ISSN | |||||||
| 収録物識別子 | 1882-7764 | |||||||
