| 作成者 |
|
|
|
| 本文言語 |
|
| 出版者 |
|
|
|
| 発行日 |
|
| 収録物名 |
|
| 巻 |
|
| 号 |
|
| 開始ページ |
|
| 終了ページ |
|
| 出版タイプ |
|
| アクセス権 |
|
| JaLC DOI |
|
| 関連DOI |
|
| 関連URI |
|
| 関連情報 |
|
| 概要 |
A new implementation technique for model-generation theorem provers (MGTP) is presented, which is particularly efficient in solving constraint satisfaction problems. We solved the so-called multienvir...onment problem by using restoration lists for destructively modified data structures. Furthermore, we introduced a new mechanism called Activation-cell which dramatically reduces the complexity of conjunctive matching, subsumption tests, and conflict tests in the proving process of MGTP. Combined with other implementation techniques including term-indexing and clause-indexing, the new MGTP written in Java shows remarkable performance compared to the previous implementations.続きを見る
|
Mendeley出力
