抄録
An effcient method for minimal model generation is presented. The method employs branching assumptions and lemmas so as to prune branches that lead to nonminimal models, and to reduce minimality tests on obtained models. This method is applicable to other approaches such as Bry's complement splitting and constrained search or Niemelä's groundedness test, and greatly improves their effciency.We implemented MM-MGTP based on the method. Experimental results with MM-MGTP show a remarkable speedup compared to MM-SATCHMO.
本文言語 | 英語 |
---|---|
ホスト出版物のタイトル | Automated Deduction - CADE-17 - 17th International Conference on Automated Deduction, Proceedings |
編集者 | David McAllester |
出版社 | Springer Verlag |
ページ | 184-199 |
ページ数 | 16 |
ISBN(電子版) | 3540676643, 9783540676645 |
DOI | |
出版ステータス | 出版済み - 2000 |
イベント | 17th International Conference on Automated Deduction, CADE 2000 - Pittsburgh, 米国 継続期間: 6 17 2000 → 6 20 2000 |
出版物シリーズ
名前 | Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science) |
---|---|
巻 | 1831 |
ISSN(印刷版) | 0302-9743 |
その他
その他 | 17th International Conference on Automated Deduction, CADE 2000 |
---|---|
Country | 米国 |
City | Pittsburgh |
Period | 6/17/00 → 6/20/00 |
All Science Journal Classification (ASJC) codes
- Theoretical Computer Science
- Computer Science(all)