| 作成者 |
|
|
|
|
|
|
|
| 本文言語 |
|
| 出版者 |
|
|
|
| 発行日 |
|
| 収録物名 |
|
| 巻 |
|
| 号 |
|
| 開始ページ |
|
| 終了ページ |
|
| 出版タイプ |
|
| アクセス権 |
|
| JaLC DOI |
|
| 関連DOI |
|
| 関連URI |
|
| 関連情報 |
|
| 概要 |
MGTP (Model Generation Theorem Prover) is a first order theorem prover based on model generation method which tries to construct Herbrand models of a given problem. We have embeded the folding-up rule... into MGTP. The folding-up rule is used to ignore duplicate subproofs. We also have embedded the splitting lemma rule into MGTP. The splitting lemma rule is used to prune redundant models. In this study, we integrate both folding-up and splitting lemma rules into MGTP in order to strengthen MGTP. We evaluate effects of the integration by proving some typical problems.続きを見る
|
Mendeley出力
