| 作成者 |
|
|
|
|
|
|
|
| 本文言語 |
|
| 出版者 |
|
|
|
| 発行日 |
|
| 収録物名 |
|
| 巻 |
|
| 号 |
|
| 開始ページ |
|
| 終了ページ |
|
| 出版タイプ |
|
| アクセス権 |
|
| JaLC DOI |
|
| 関連DOI |
|
| 関連URI |
|
| 関連情報 |
|
| 概要 |
Factorization used in resolution provers can be effectively applied to model generation provers in order to eliminate the redundancies in case splittings. We propose a new factorization-based techniqu...e called a static/dynamic lemma generation, and present its efficient implementation on MGTP(Model Generation Theorem Prover). Experimental results obtained by running MGTP with the technique for several problems from the TPTP library demonstrate the effectiveness of the proposed technique and implementation.続きを見る
|
Mendeley出力
