分岐補題の抽出による極小モデル生成の効率化

• 長谷川 隆三

  九州大学大学院システム情報科学研究院

• 藤田 博

  九州大学大学院システム情報科学研究院

• 越村 三幸

  九州大学大学院システム情報科学研究院

書誌事項

タイトル別名

• Improving the Efficiency of Minimal Model Generation by Extracting Branching Lemmas
• ブンキホ ダイ ノ チュウシュツ ニ ヨル キョクショウ モデル セイセイ ノ コウリツカ

抄録

We present an efficient method for minimal model generation. 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. Branching lemmas are extracted from a subproof of a disjunct, and work as factorization. This method is applicable to other approaches such as Bry’s constrained search or Niemelä’s groundedness test, and greatlyimpro ves their efficiency. We implemented MM-MGTP based on the method. Experimental results with MM-MGTP show a remarkable speedup compared to MM-SATCHMO.

収録刊行物

• 人工知能学会論文誌

  人工知能学会論文誌 16 234-245, 2001

  一般社団法人 人工知能学会

キーワード

• model generation
• minimal models
• automated reasoning
• theorem proving
• SATCHMO
• MGTP

詳細情報

• CRID: 1390001205108171520
• NII論文ID: 10015769889
• NII書誌ID: AA11579226
• DOI: 10.1527/tjsai.16.234
• ISSN: 13468030
• ISSN: 13460714
• NDL書誌ID: 5987144
• Web Site: https://ndlsearch.ndl.go.jp/books/R000000004-I5987144
• Web Site: http://www.jstage.jst.go.jp/article/tjsai/16/2/16_2_234/_pdf
• 本文言語コード: ja
• データソース種別:
  • JaLC
  • NDL
  • Crossref
  • CiNii Articles
• 抄録ライセンスフラグ: 使用不可