| 作成者 |
|
|
|
|
|
|
|
| 本文言語 |
|
| 出版者 |
|
|
|
| 発行日 |
|
| 収録物名 |
|
| 巻 |
|
| 開始ページ |
|
| 終了ページ |
|
| 出版タイプ |
|
| アクセス権 |
|
| JaLC DOI |
|
| 関連DOI |
|
| 関連URI |
|
| 関連情報 |
|
| 概要 |
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 a...nd 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.続きを見る
|
Mendeley出力
