| 作成者 |
|
|
|
|
|
|
|
| 本文言語 |
|
| 出版者 |
|
|
|
| 発行日 |
|
| 収録物名 |
|
| 巻 |
|
| 号 |
|
| 開始ページ |
|
| 終了ページ |
|
| 出版タイプ |
|
| アクセス権 |
|
| JaLC DOI |
|
| 関連DOI |
|
| 関連URI |
|
| 関連情報 |
|
| 概要 |
We present a new method to eliminate redundant inferences caused by case-splitting in MGTP. There are two types of redundancies eliminated by the method: One is that the same sub-proof tree may be gen...erated at several descendant nodes after a case-splitting occurs. Another is caused by useless model candidate extensions with irrelevant non-Horn clauses. Both types of redundancies can be eliminated by combining the folding-up function that conveys unit lemmata obtained from solved descendant nodes to a proper antecedent node and the NHM function that suppresses useless model extensions. The method has been implemented in MGTP. We evaluate its effects on a UNIX workstation for some typical problems taken from the TPTP problem library.続きを見る
|
Mendeley出力
