| 作成者 |
|
|
|
|
|
| 本文言語 |
|
| 出版者 |
|
|
|
| 発行日 |
|
| 収録物名 |
|
| 巻 |
|
| 号 |
|
| 開始ページ |
|
| 終了ページ |
|
| 出版タイプ |
|
| アクセス権 |
|
| JaLC DOI |
|
| 関連DOI |
|
| 関連URI |
|
| 関連情報 |
|
| 概要 |
Non-Horn magic sets(NHM) method transforms a given clause set into a set of clauses simulating backward reasoning and those for controlling forward reasoning so as to prune the search space. To preser...ve the range-restricted condition, the transformation needs to attach an adornment to a predicate to show binding information of its arguments. However, introducing adornments causes combinatorial explosion of the number of transformed clauses because the number of adornments may increase exponentially. This paper presents four methods to decrease the number of transformed clauses: (1) obtaining necessary adornments by statical analysis, (2) extracting minimal adornments from necessary adornments, (3) calculating necessary adornments dynamically, and (4) transformation without adornments. These methods have been implemented on a UNIX workstation. We evaluated their effects by proving some problems in the TPTP problem library.続きを見る
|
Mendeley出力
